Test-Driven Development (TDD) is the practice of attempting to use the software you intend to write, before you write it. The premise is straightforward, but the specifics of applying it in different domains can be co...
详细信息
ISBN:
(纸本)9789897580659
Test-Driven Development (TDD) is the practice of attempting to use the software you intend to write, before you write it. The premise is straightforward, but the specifics of applying it in different domains can be complex. In this paper, we provide aTDD approach for language development. The essence is to apply TDD at each of four levels of language processing, hence we call our approach Multi-Level TDD, or MLTDD. MLTDD can be applied to programming languages, preprocessors, domain specific languages, and transformation engines. MLTDD was used to build Umple, a model-oriented programming language available for java, Ruby, and PHP. We present two case studies where this approach was implemented to develop two other domain specific languages.
The proceedings contain 20 papers. The topics discussed include: Quarantine: a framework to mitigate memory errors in JNI applications;portable and accurate collection of calling-context-sensitive byte-code metrics fo...
ISBN:
(纸本)9781450309356
The proceedings contain 20 papers. The topics discussed include: Quarantine: a framework to mitigate memory errors in JNI applications;portable and accurate collection of calling-context-sensitive byte-code metrics for the java virtual machine;the java virtual machine in retargetable, high-performance instruction set simulation;a DSL for writing type systems for Xtext languages, space-based multi-core programming in java;Habanero-java: the new adventures of old X10;ejIP: a TCP/IP stack for embedded java;the soul tool suite for querying programs in symbiosis with Eclipse;Jazz2: a flexible and extensible framework for structural testing;object reuse and behavior adaptation in java-like languages;trace-based compilation for the java hotspot virtual machine;tool demonstration: overseer - low-level hardware monitoring and management for java;and optimized memory management for class metadata in a JVM.
Although there exists many Semantic Web tools and APIs to help building semantic web applications, java EE 3-tier architecture has been largely used in developing large enterprise applications. It is proved to be comp...
详细信息
A unification method based on the λse-style of explicit substitution is proposed. This method together with appropriate translations, provide a Higher Order Unification (HOU) procedure for the pure λ-calculus. Our m...
详细信息
ISBN:
(纸本)1581132654
A unification method based on the λse-style of explicit substitution is proposed. This method together with appropriate translations, provide a Higher Order Unification (HOU) procedure for the pure λ-calculus. Our method is influenced by the treatment introduced by Dowek, Hardin and Kirchner using the λσ-style of explicit substitution. Correctness and completeness properties of the proposed λse-unification method are shown and its advantages, inherited from the qualities of the λse-calculus, are pointed out. Our method needs only one sort of objects: terms. And in contrast to the HOU approach based on the λσ-calculus, it avoids the use of substitution objects. This makes our method closer to the syntax of the λ-calculus. Furthermore, detection of redices depends on the search for solutions of simple arithmetic constraints which makes our method more operational than the one based on the λσ-style of explicit substitution.
The operational semantics of linear logic programming languages is given in terms of goal-driven sequent calculi. The proof-theoretic presentation is the natural counterpart of the top-down semantics of traditional lo...
详细信息
ISBN:
(纸本)1581132654
The operational semantics of linear logic programming languages is given in terms of goal-driven sequent calculi. The proof-theoretic presentation is the natural counterpart of the top-down semantics of traditional logic programs. In this paper we investigate the theoretical foundation of an alternative operational semantics based on a bottom-up evaluation of linear logic programs via a fixpoint operator. The bottom-up fixpoint semantics is important in applications like active databases, and, more in general, for program analysis and verification. As a first case-study, we consider Andreoli and Pareschi's LO [4] enriched with the constant 1. For this language, we give a fixpoint semantics based on an operator defined in the style of TP. We give an algorithm to compute a single application of the fixpoint operator where constraints are used to represent in a finite way possibly infinite sets of provable goals. Furthermore, we show that the fixpoint semantics for propositional LO without the constant 1 can be computed after finitely many steps. To our knowledge, this is the first attempt to define an effective fixpoint semantics for LO. We hope that our work will open interesting perspectives for the analysis and verification of linear logic programming languages.
Web services have emerged as a technology for designing and composing distributed applications. Recent research increasingly addressed the need to adapt such systems based on changing requirements and environmental co...
详细信息
This paper analyzes and thinks the advantages and disadvantages of traditional teaching methods of java course. The thinking and practical application of the hybrid teaching mode based on the superstar platform are co...
详细信息
We introduce and develop the notion of symmetric monoidal sketch. Every symmetric monoidal sketch generates a generic model. If the sketch is commutative and single-sorted, the generic model can be characterised as a ...
详细信息
ISBN:
(纸本)1581132654
We introduce and develop the notion of symmetric monoidal sketch. Every symmetric monoidal sketch generates a generic model. If the sketch is commutative and single-sorted, the generic model can be characterised as a free structured category on the small category 1. Moreover, there is a comonad Mods (S,-) on the category SymMons of small symmetric monoidal categories and strict symmetric monoidal functors such that the category of Mods(S,-)-coalgebras describes the above-mentioned structure. Given a commutative single-sorted sketch, the construction sending a small symmetric monoidal category to the category of models of the sketch in it provides a right adjoint to the forgetful functor from the category of coalgebras to SymMons. We investigate specific cases generated by the Eckmann-Hilton argument, which allows a simple characterisation of the constructions. This accounts for the various categories of wiring currently being investigated in modelling concurrency, as well as providing a basis for understanding the axiomatically generated categories in axiomatic domain theory and in presheaf models of concurrency.
Tableau-based proof systems can be elegantly specified and directly executed by a tabled Logic programming (LP) system. Our experience with the XMC model checker shows that such an encoding can be used to search for t...
详细信息
ISBN:
(纸本)1581132654
Tableau-based proof systems can be elegantly specified and directly executed by a tabled Logic programming (LP) system. Our experience with the XMC model checker shows that such an encoding can be used to search for the existence of a proof very efficiently. However, the users of a tableau system are often interested in getting sufficient evidence (in terms of the tableau proof rules) on why a proof does or does not exist. In this paper, we address the problem of constructing such an evidence without introducing any additional computational overhead to the proof search. A tabled LP system maintains a memo table of "lemmas" that were tried and possibly proved during query evaluation. We propose the concept of justifier for extracting sufficient. evidence for the truth or falsehood of literals in a logic program, by post-processing the memo tables created during query evaluation. Based on this logic program justifier, we show how to construct evidence for the presence/absence of tableau in a tableau-based proof system. We provide experimental results showing the effectiveness of the justifier in constructing succinct evidence of the evaluation performed by the XMC model checker. Finally we discuss the role of the justifier as a programming abstraction for encoding efficient algorithms as tabled logic programs.
Sharing, a domain due to D. Jacobs and A. Langen for the analysis of logic programs, derives useful aliasing information. It is well-known that a commonly used core of techniques, such as the standard integration of S...
详细信息
ISBN:
(纸本)1581132654
Sharing, a domain due to D. Jacobs and A. Langen for the analysis of logic programs, derives useful aliasing information. It is well-known that a commonly used core of techniques, such as the standard integration of Sharing with freeness and linearity information, can significantly improve the precision of Sharing. However, a number of other proposals for refined domain combinations have been circulating for years. One feature that is common to these proposals is that they do not seem to have undergone a thorough experimental evaluation even with respect to the expected precision gains. In this paper, we discuss and/or experimentally evaluate: helping Sharing with definitely ground variables computed with Pos;the incorporation of explicit structural information into the domain of analysis;more sophisticated ways of integrating Sharing and Pos;the issue of reordering the bindings in the computation of the abstract mgu;an original proposal concerning the addition of a domain recording the set of variables that are deemed to be ground or free;a more refined way of using linearity to improve the analysis;the issue of whether tracking compoundness allows to compute more precise sharing information;and, finally, the recovery of hidden information in the combination of Sharing with the usual domain for freeness.
暂无评论