Program Development in Computational Logic

Since the early days of programming and automated reasoning, researchers have developed methods for systematically constructing programs from their specifications. Especially the last decade has seen a flurry of activities including the advent of specialized conferences, such as LOPSTR, covering the synthesis of programs in computational logic. In this paper we analyze and compare three state-of-the-art methods for synthesizing recursive programs in computational logic. The three approaches are constructive/deductive synthesis, schema-guided synthesis, and inductive synthesis. Our comparison is carried out in a systematic way where, for each approach, we describe the key ideas and synthesize a common running example. In doing so, we explore the synergies between the approaches, which we believe are necessary in order to achieve progress over the next decade in this field.

In this paper we demonstrate a refinement calculus for logic programs, which is a framework for developing logic programs from specifications. The paper is written in a tutorial-style, using a running example to illustrate how the refinement calculus is used to develop logic programs. The paper also presents an overview of some of the advanced features of the calculus, including the introduction of higher-order procedures and the refinement of abstract data types.

Most logic programming languages actually provide some kind of dynamic scheduling to increase the expressive power and to control execution. Input consuming derivations have been introduced to describe dynamic scheduling while abstracting from the technical details. In this paper we review and compare the different proposals given in [9], [10] and [12] for denotational semantics of programs with input consuming derivations. We also show how they can be applied to termination analysis.

One recent advance in program development has been the application of abstract interpretation to verify the partial correctness of a (constraint) logic program. Traditionally forwards analysis has been applied that starts with an initial goal and traces the execution in the direction of the control-flow to approximate the program state at each program point. This is often enough to verify assertions that a property holds. The dual approach is to apply backwards analysis to propagate properties of the allowable states against the control-flow to infer queries for which the program will not violate any assertion. Backwards analysis also underpins other program development tasks such as verifying the termination of a logic program or proving that a logic program with a delay mechanism cannot reduce to a state that contains sub-goals which suspend indefinitely. This paper reviews various backwards analyses that have been proposed for logic programs, identifying common threads in these techniques. The analyses are explained through a series of worked examples. The paper concludes with some suggestions for research in backwards analysis for logic program development.

In this work, we develop a binding-time analysis for the logic programming language Mercury. We introduce a precise domain of binding-times, based on the type information available in Mercury programs, that allows the analyser to reason with partially static data structures. The analysis is polyvariant, and deals with the module structure and higher-order capabilities of Mercury programs.

Context-sensitive analysis provides information which is potentially more accurate than that provided by context-free analysis. Such information can then be applied in order to validate/debug the program and/or to specialize the program obtaining important improvements. Unfortunately, context-sensitive analysis of modular programs poses important theoretical and practical problems. One solution, used in several proposals, is to resort to context-free analysis. Other proposals do address context-sensitive analysis, but are only applicable when the description domain used satisfies rather restrictive properties. In this paper, we argue that a general framework for context-sensitive analysis of modular programs, i.e., one that allows using all the domains which have proved useful in practice in the non-modular setting, is indeed feasible and very useful. Driven by our experience in the design and implementation of analysis and specialization techniques in the context of CiaoPP, the Ciao system preprocessor, in this paper we discuss a number of design goals for context-sensitive analysis of modular programs as well as the problems which arise in trying to meet these goals. We also provide a high-level description of a framework for analysis of modular programs which does substantially meet these objectives. This framework is generic in that it can be instantiated in different ways in order to adapt to different contexts. Finally, the behavior of the different instantiations w.r.t. the design goals that motivate our work is also discussed.

Formal verification of reactive concurrent systems is important since many hardware and software components of our computing environment can be modeled as reactive concurrent systems. Algorithmic techniques for verifying concurrent systems such as model checking can be applied to finite state systems only. This chapter investigates the verification of a common class of infinite state systems, namely parameterized systems. Such systems are parameterized by the number of component processes, for example an n-process token ring for any n. Verifying the entire infinite family represented by a parameterized system lies beyond the reach of traditional model checking. On the other hand, deductive techniques to verify infinite state systems often require substantial user guidance.

The goal of this work is to integrate algorithmic and deductive techniques for automating proofs of temporal properties of parameterized concurrent systems. Here, the parameterized system to be verified and the temporal property are encoded together as a logic program. The problem of verifying the temporal property is then reduced to the problem of determining equivalence of predicates in this logic program. These predicate equivalences are established by transforming the program such that the semantic equivalence of the predicates can be inferred from the structure of their clauses in the transformed program.

For transforming the predicates, we use the well-established unfold/fold transformations of logic programs. Unfolding represents a step of resolution and can be used to evaluate the base case and the finite part of the induction step in an induction proof. Folding and other transformations represent deductive reasoning and can be used to recognize the induction hypothesis. Together these transformations are used to construct induction proofs of temporal properties. Strategies are developed to help guide the application of the transformation rules. The transformation rules and strategies have been implemented to yield an automatic and programmable first order theorem prover for parameterized systems. Case studies include multi-processor cache coherence protocols and the Java Meta-Locking protocol from Sun Microsystems. The program transformation based prover has been used to automatically prove various safety properties of these protocols.

We propose a set of transformation rules for constraint logic programs with negation. We assume that every program is locally stratified and, thus, it has a unique perfect model. We give sufficient conditions which ensure that the proposed set of transformation rules preserves the perfect model of the programs. Our rules extend in some respects the rules for logic programs and constraint logic programs already considered in the literature and, in particular, they include a rule for unfolding a clause with respect to a negative literal.

We present the latest version of the logen partial evaluation system for logic programs. In particular we present new binding-types, and show how they can be used to effectively specialise a wide variety of interpreters. We show how to achieve Jones-optimality in a systematic way for several interpreters. Finally, we present and specialise a non-trivial interpreter for a small functional programming language. Experimental results are also presented, highlighting that the logen system can be a good basis for generating compilers for high-level languages.

The procedural interpretation of logic programs and queries is parametric to the selection rule, i.e. the rule that determines which atom is selected in each resolution step. Termination of logic programs and queries depends critically on the selection rule. In this survey, we present a unified view and comparison of seven notions of universal termination considered in the literature, and the corresponding classes of programs. For each class, we focus on a sufficient, and in most cases even necessary, declarative characterisation for determining that a program is in that class. By unifying different formalisms and making appropriate assumptions, we are able to establish a formal hierarchy between the different classes and their respective declarative characterisations.

Reasoning about termination is a key issue in logic program development. One classic technique for proving termination is to construct a well-founded order on goals that decreases between successive goals in a derivation. In practise, this is achieved with the aid of a level mapping that maps atoms to natural numbers. This paper examines why it can be difficult to base termination proofs on natural level mappings that directly relate to the recursive structure of the program. The notions of bounded-recurrency and bounded-acceptability are introduced to alleviate these problems. These concepts are equivalent to the classic notions of recurrency and acceptability respectively, yet provide practical criteria for constructing termination proofs in terms of natural level mappings for definite logic programs. Moreover, the construction is entirely modular in that termination conditions are derived in a bottom-up fashion by considering, in turn, each the strongly connected components of the program.

This paper describes a method for proving termination of queries to logic programs based on abstract interpretation. The method uses query-mapping pairs to abstract the relation between calls in the LD-tree associated with the program and query. Any well founded partial order for terms can be used to prove the termination. The ideas of the query-mapping pairs approach have been implemented in SICStus Prolog in a system called TermiLog, which is available on the web. Given a program and query pattern the system either answers that the query terminates or that there may be non-termination. The advantages of the method are its conceptual simplicity and the fact that it does not impose any restrictions on the programs.

Mercury is a logic programming language that is considerably faster than traditional Prolog implementations, but lacks support for full unification. HAL is a new constraint logic programming language specifically designed to support the construction of and experimentation with constraint solvers, and which compiles to Mercury. In this paper we describe the HAL Herbrand constraint solver and show how by using PARMA bindings, rather than the standard WAM representation, we can implement a solver that is compatible with Mercury’s term representation. This allows HAL to make use of Mercury’s more efficient procedures for handling ground terms, and thus achieve Mercury-like efficiency while supporting full unification. An important feature of HAL is its support for user-extensible dynamic scheduling since this facilitates the creation of propagation-based constraint solvers. We have therefore designed the HAL Herbrand constraint solver to support dynamic scheduling. We provide experiments to illustrate the efficiency of the resulting system, and systematically compare the effect of different declarations such as type, mode and determinism on the resulting code.