the proceedings contain 17 papers. the special focus in this conference is on Invited Talk and Tutorials. the topics include: Algebraic specification and program development by stepwise refinement extended abstract;pr...
ISBN:
(纸本)3540676287
the proceedings contain 17 papers. the special focus in this conference is on Invited Talk and Tutorials. the topics include: Algebraic specification and program development by stepwise refinement extended abstract;proof obligations of the b formal method;constraint logicprogramming applied to model checking;on dynamic aspects of OOD frameworks in component-based software development in computational logic;infinite state model checking by abstract interpretation and program specialisation;mode analysis domains for typed logicprograms;imperative program specialisation;specialising finite domain programs using polyhedra;roles of program extension;transformation of left terminating programs;transformation rules for logicprograms with goals as arguments;making mercury programs tail recursive;the replacement operation for CCP programs;annotations for prolog - a concept and runtime handling;verification by testing for recursive program schemes;combined static and dynamic assertion-based debugging of constraint logicprograms and context-moving transformations for function verification.
We review and discuss here some of the existing approaches based on CLP (Constraint logicprogramming) for verifying properties of various kinds of state-transition systems.
ISBN:
(纸本)3540676287
We review and discuss here some of the existing approaches based on CLP (Constraint logicprogramming) for verifying properties of various kinds of state-transition systems.
Various formalizations of the concept of "refinement step" as used in the formal development of programs from algebraic specifications are presented and compared.
ISBN:
(纸本)3540676287
Various formalizations of the concept of "refinement step" as used in the formal development of programs from algebraic specifications are presented and compared.
We illustrate the use of logicprogramming techniques for finite model checking of CTL formulae. We present a technique for infinite state model checking of safety properties based upon logic, program specialisation a...
详细信息
ISBN:
(纸本)3540676287
We illustrate the use of logicprogramming techniques for finite model checking of CTL formulae. We present a technique for infinite state model checking of safety properties based upon logic, program specialisation and analysis techniques. the power of the approach is illustrated on several examples. For that, the efficient tools LOGEN and ECCE are used. We discuss how this approach has to be extended to handle more complicated infinite state systems and to handle arbitrary CTL formulae.
the replacement is a very powerful transformation operation which - both within the functional paradigm as well as within the logicprogramming one - can mimic the most common transformation operations such as unfold,...
详细信息
ISBN:
(纸本)3540676287
the replacement is a very powerful transformation operation which - both within the functional paradigm as well as within the logicprogramming one - can mimic the most common transformation operations such as unfold, fold, switching, distribution. Because of this flexibility, it can be incorrect if used without specific applicability conditions. In this paper we present applicability conditions which ensure the correctness of the replacement operation in the context of Concurrent Constraint programs. Furthermore we show that, under these conditions, the replacement generalizes boththe unfolding operation as well as a restricted form of folding operation.
A formal and effective approach to the extension of the computational behaviour of logicprograms is presented. the approach builds upon the following concepts. the extension of computational behaviour is modelled by ...
详细信息
ISBN:
(纸本)3540676287
A formal and effective approach to the extension of the computational behaviour of logicprograms is presented. the approach builds upon the following concepts. the extension of computational behaviour is modelled by semantics-preserving programtransformations. Several basic roles involved in such transformations are identified. Every transformation defined solely in terms of the basic roles will be semantics-preserving by definition. Functional meta-programs on logic object programs are used to specify the basic roles and to derive programming techniques in the style of stepwise enhancement. thus, the process of extending the computational behaviour of logicprograms is regarded as disciplined meta-programming.
We introduce a logic language where predicate symbols may have both terms and goals as arguments. We define its operational semantics by extending SLD-resolution withthe leftmost selection rule, and we propose a set ...
详细信息
ISBN:
(纸本)3540676287
We introduce a logic language where predicate symbols may have both terms and goals as arguments. We define its operational semantics by extending SLD-resolution withthe leftmost selection rule, and we propose a set of transformation rules for manipulating programs written in that language. these transformation rules are shown to be correct in the sense that they preserve the chosen operational semantics. this logic language has higher order capabilities which turn out to be very powerful for the derivation of efficient logicprograms. In particular, in our language we can avoid the problem of goal rearrangement which is often encountered during programtransformation. Moreover, goals as arguments allow us to perform on logicprograms transformation steps similar to the ones performed on functional programs when using higher order generalizations and continuation arguments.
Precise mode information is important for compiler optimisations and in program development tools. Within the framework of abstract compilation, the precision of a mode analysis depends, in part, on the expressiveness...
详细信息
ISBN:
(纸本)3540676287
Precise mode information is important for compiler optimisations and in program development tools. Within the framework of abstract compilation, the precision of a mode analysis depends, in part, on the expressiveness of the abstract domain and its associated abstraction function. this paper considers abstract domains for polymorphically typed logicprograms and shows how specialised domains may be constructed for each type in the program. these domains capture the degree of instantiation to a high level of precision. By providing a generic definition of abstract unification, the abstraction of a program using these domains is formalised. the domain construction procedure is fully implemented using the Godel language and tested on a number of example programs to demonstrate the viability of the approach.
the semantics of an imperative programming language can be expressed as a program in a declarative constraint language. Not only does this render the semantics executable, but it opens up the possibility of applying t...
详细信息
ISBN:
(纸本)3540676287
the semantics of an imperative programming language can be expressed as a program in a declarative constraint language. Not only does this render the semantics executable, but it opens up the possibility of applying to imperative languages the advances made in program analysis and transformation of declarative languages. We propose a method for carrying out partial evaluation of imperative programs, using partial evaluation in a declarative language, but returning the results in the syntax of the imperative program which is to be partially evaluated. the approach uses a special form of the semantics and program points to aid partial evaluation. the partially evaluated semantics program is represented as a labelled directed graph. An algorithm for reconstructing an imperative program from the graph and the residual program is presented. Constraints provide a means through which information is propagated inside both branches of a conditional, the body of a loop, and along def-use chains in the program. the method provides a framework for constructing a partial evaluator for any imperative programming language, by writing down its semantics as a declarative program (a constraint logicprogram, in the approach shown here).
We propose a general framework for assertion-based debugging of constraint logicprograms. Assertions are linguistic constructions for expressing properties of programs. We define several assertion schemas for writing...
详细信息
ISBN:
(纸本)3540676287
We propose a general framework for assertion-based debugging of constraint logicprograms. Assertions are linguistic constructions for expressing properties of programs. We define several assertion schemas for writing (partial) specifications for constraint logicprograms using quite general properties, including user-defined programs. the framework is aimed at detecting deviations of the program behavior (symptoms) with respect to the given assertions, either at compile-time (i.e., statically) or run-time (i.e., dynamically). We provide techniques for using information from global analysis both to detect at compile-time assertions which do not hold in at least one of the possible executions (i.e., static symptoms) and assertions which hold for all possible executions (i.e., statically proved assertions). We also provide programtransformations which introduce tests in the program for checking at run-time those assertions whose status cannot be determined at compile-time. Boththe static and the dynamic checking are provably safe in the sense that all errors flagged are definite violations of the specifications. Finally, we report briefly on the currently implemented instances of the generic framework.
暂无评论