Elan(ID:3458/ela003)Constraint logic programConstraint handling logic from france from the ELAN home page: "the ELAN system provides an environment for specifying and prototyping deduction systems in a language based on rules controlled by strategies. Its purpose is to support the design of theorem provers, logic programming languages, constraints solvers and decision procedures and to offer a modular framework for studying their combination. ELAN takes from functional programming the concept of abstract data types and the function evaluation principle based on rewriting. But rewriting is inherently non-deterministic since several rules can be applied at different positions in a same term, and in ELAN, a computation may have several results. This aspect is taken into account through choice operations and a backtracking capability. One of the main originality of the language is to provide strategy constructors to specify whether a function call returns several, at-least one or only one result. This declarative handling of non-determinism is part of a strategy language allowing the programmer to specify the control on rules application. This is in contrast to many existing rewriting-based languages where the term reduction strategy is hard-wired and not accessible to the designer of an application. The strategy language offers primitives for sequential composition, iteration, deterministic and non-deterministic choices of elementary strategies that are labelled rules. From these primitives, more complex strategies can be expressed. In addition the user can introduce new strategy operators and define them by rewrite rules. Evaluation of strategy application is itself based on rewriting. So the simple and well-known paradigm of rewriting provides both the logical framework in which deduction systems can be expressed and combined, and the evaluation mechanism of the language." References: The present volume is an annotated bibliography which attempts to provide an up-to-date overview of past and present work on algebraic specification. No attempt is made to provide a coherent introduction to the topic for beginners the intention is rather to provide a guide to the current literature for researchers in algebraic specification and neighbouring fields. Some indications of how the different approaches are related are included. ps Extract: Elan, a logical framework based on rewriting logic Elan, a logical framework based on rewriting logic Rewriting logic [...] appears both as a semantic framework for specification of systems and languages, well-suited to concurrency, parallel programming, object-oriented specification, and as a logical framework for representing logics. In this direction, logic programming in a broad sense, theorem proving and constraint solving can be described in a uniform way by giving the syntax of formulas, a set of axioms, a set of deduction rules, a proof calculus making precise how proofs are built, altogether with one or a class of models. These three computational processes can be formulated within rewriting logic that provides the uniform framework to reason about combination and integration of these three paradigms. ELAN is a logical framework that allows the formalisation of various logics and constraint solvers. The rewriting logic is the formal basis of the evaluation mechanism in ELAN. Rules may be conditional and are enriched by local variables. A notion of strategy is added and a computational system is a rewrite theory enriched by a set of strategies controlling application of rules and restricting the search space of computation. A strategy language is provided with concatenation, iteration and choice operators. The system is used to prototype, experiment and study the combination of different computational systems that provide basis for constraint solving, theorem proving and logic programming paradigms. Different deduction processes using constraints have been designed in ELAN, such as a narrowing process with constraints to solve queries in theories defined by rewrite rules, the kernel of a constraint logic programming language using for instance a constraint solver for systems of equations in commutative theories. In [...], a completion process using a basic superposition strategy expressed with constraints, is described in ELAN. The strategy language is used for experimenting various simlification strategies in this context. Another significant example developed in ELAN is a higher-order unification algorithm based on Lambda-calculus with explicit substitutions. A compiler of ELAN in C considerably improves the efficiency of the interpreted system. Extract: Extended ML Extended ML The long-term goal of work on Extended ML is to provide a practical framework for formal development of Standard ML programs together with an integrated suite of computer-based specification and development support tools and complete mathematical foundations to substantiate claims of correctness. The complete formal definition of the Extended ML language [533] constitutes an important milestone in this programme, necessary to provide a basis for further research on foundations and tools. One of the key issues that had to be resolved was the design of a logic suitable for describing properties of Standard ML programs, taking into account features like recursive type and function definitions, exceptions, polymorphism, and non-termination. A number of errors in the Standard ML semantics [679] have been discovered in the course of this work [526]. Work has begun on rules for proving theorems about EML specifications, to be used in verifying correctness conditions that arise in the course of formal development. Research has so far concentrated on equality reasoning [530] and quantifier rules. The length and requisite formality of the definition of Extended ML renders it rather difficult to penetrate. Accordingly, [532, 534] provides an informal overview of the definition, explaining most of the main issues involved and justifying some of the choices taken. Extract: Reusability The demand for reusability originates from economic considerations and attempts towards standardization. Rather than always starting from scratch, the use of existing components is cheaper and also less error-prone. A central problem for the identification and the correct use of reusable components is the abstract description of such components. A formal specification is the only form of description that can serve as a basis for a correctness proof; it can be processed automatically and it establishes a degree of confidence in the functionality of the component that is particularly important if a component has to be modified before being reused. Goguen [404] proposes the algebraic specification language OBJ as well-suited for the design of reusable software systems. A component's interface is specified as an abstract data type and may be parameterized by other components. Combination of components is possible by instantiation using appropriate fitting morphisms. A similar approach is used in Extended ML [836], [848]. In ACT TWO [315] components are modules, which consist of two interface specifications, i.e. an export specification and an import specification, and a body specification which implements the export specification in terms of the import specification. Similarly, in LARCH [445], a component consists of a pair, an "abstract" interface specification and an implementation. Here the implementation is written in a conventional programming language. A similar distinction between a requirement and a design specification is made in PAnndA-S, the language of the PROSPECTRA project [138], based on the notion of visible and private interface in Ada. Ada bodies are generated semi-automatically by transformation. In the approach of [655] a component consists of four parts at four different levels of abstraction: a requirement specification, a design specification, a source program and object code. Components are written in a so-called wide spectrum language which provides facilities for system design and software development at many levels of abstraction. Matsumoto uses Ada, which has as a consequence that the requirement specification is merely an informal description. CIP-L [54] and COLD [341] are two languages which include algebraic specifications as well as predicative and imperative language styles in one coherent framework and therefore are better suited for such an approach. In the object-oriented approach of [675] a reusable component is represented by a graph of object-oriented programs, each node of which stands for one level of abstraction in the description of the software. In the approach of the ESPRIT-project DRAGON [945], a reusable component consists of a tree of algebraic specifications, where similarly to [675], each node of the tree is an instance of a certain level of an abstraction of the program with the root being the most "abstract" formal specification and the leaves representing the "concrete" implementations. A methodology for reusing components is described in [947]. in Proc. of JSSST 3rd Fuji International Symposium on Functional and Logic Programming. 1998 view details in Proc. of JSSST 3rd Fuji International Symposium on Functional and Logic Programming. 1998 view details in Proc. of JSSST 3rd Fuji International Symposium on Functional and Logic Programming. 1998 view details in Proc. of JSSST 3rd Fuji International Symposium on Functional and Logic Programming. 1998 view details in Proc. of JSSST 3rd Fuji International Symposium on Functional and Logic Programming. 1998 view details in Gabbay, D.M. and M. de Rijke editors. Frontiers of Combining Systems 2 Research Studies Press/Wiley, 1999. view details in Gabbay, D.M. and M. de Rijke editors. Frontiers of Combining Systems 2 Research Studies Press/Wiley, 1999. view details in Gabbay, D.M. and M. de Rijke editors. Frontiers of Combining Systems 2 Research Studies Press/Wiley, 1999. view details in Gabbay, D.M. and M. de Rijke editors. Frontiers of Combining Systems 2 Research Studies Press/Wiley, 1999. view details Resources |