Formal Construction of Distributed Programs (with an example of protocol construction).
----------------------------------------------------------
Jean-Raymond Abrial

We shall present a method for systematically constructing (and formally proving) distributed programs. Emphasis will be put on the discovery of so-called invariant and easiness of proofs.



Data Flow Semantics for (C)LP and Applications.
---------------------------------------------
Livio Colussi

An alternative operational model for constraint logic programs, formalized as a transition system, is discussed and used to define an operational semantics T. Then an equivalent fixpoint semantics F is defined: a dataflow graph is assigned to a program, and a consequence operator on tuples of sets of constraint is given whose least fixpoint determines one set of constraints for each node of the dataflow graph. Then the correctness of F w.r.t. T is established, by means of an intermediate semantics O. Applications of F and O are:

References

[CMM95a] Livio Colussi, Elena Marchiori, Massimo Marchiori. A Dataflow Semantics for Constraint Logic Programs. In Proceedings of the Seventh International Symposium on Programming Languages, Implementations, Logics and Programs (PLILP'95), LNCS 982, pages 431-448, Springer-Verlag, 1995.

[CMM95b] Livio Colussi, Elena Marchiori, Massimo Marchiori. On Termination of Constraint Logic Programs. In Proceedings of the First International Conference on Principles and Practice of Constraint Programming (CP'95), LNCS 976, pages 431-448, Springer-Verlag, 1995.



Proving properties of logic programs by abstract diagnosis
----------------------------------------------------------
Giorgio Levi

Declarative diagnosis (debugging) [Shapiro82,Ferrand87,Lloyd87a,Ferrand93,CominiLV95a] is a technique which allows one to prove the correctness and completeness of a program with respect to a specification of the intended program behaviour. In the case of incorrect and incomplete programs, the diagnosis gives information on the wrong and missing answers. The specification is the intended semantics [[P]] (for example, the intended least Herbrand model). As shown in [CominiLV95a], one of the nice features of this technique is the fact that we can prove correctness and completeness without actually constructing the semantics of the program. It is in fact sufficient to compare the specification $I$ and the result ($T_{P}(I)$) of the application of the immediate consequences operator $T_{P}$ to $I$. The immediate consequences operator has to be chosen so as to model the semantics considered in the specification (for example, the least Herbrand model, the set of atomic consequences or the computed answers). The comparison between $I$ and $T_{P}(I)$ allows us to verify (partial) program correctness. Moreover it allows us to verify program completeness for a very large class of logic programs (accettable programs as defined in [AptP93]). Finally it provides meaningful information about wrong and missing clauses. The diagnosis can be implemented by simple ``top-down'' meta-interpreters, which query the user (oracle) to get the information on the intended behaviour. The problem with the above technique is that it is not effective since specifications are usually infinite. It becomes effective if one considers a (finite) abstract semantics, defined according to abstract interpretation theory [CousotC77]. This leads to an extension of the theory, called abstract diagnosis [CominiLV94,CominiLV95], which allows one to tackle the problems of determining correctness and completeness with respect to a specification of the program properties represented by the abstract semantics. Examples of useful program properties for logic programs which can be handled by abstract diagnosis are types and groundness dependencies. For each abstraction $\alpha$, we need an abstract immediate consequences operator $T_{P}^{\alpha}$, which computes on the abstract domain and whose least fixpoint is the abstract semantics $[[P]]^{\alpha}$. Abstract computations generally lead to a loss of precision (approximation): $[[P]]^{\alpha}\ge \alpha([[P]])$, where $\ge$ is the partial order relation of the abstract domain. This makes the results of abstract diagnosis weaker. Namely we can verify correctness, but not completeness. On the other side, we can detect incompleteness bugs and cannot detect incorrectness bugs. The (relative) precision of the abstraction is relevant. We have determined a class of abstractions, for which the abstract semantics computed by $T_{P}^{\alpha}$ is the most precise (these are the semi-denotational observables in the semantic framework in [CominiLM95]). This class includes several abstract domains proposed for type analysis and the domain POS, proposed for groundness analysis [ArmstrongMSS95].

References

[AptP93] K.R. Apt and D.Pedreschi. Reasoning about termination of pure {PROLOG} programs. Information and Computation, 106(1):109--157, 1993.

[ArmstrongMSS95] T.Armstrong, K.Marriott, P.Schachte, and H.S{\o}ndergaard. Two Classes of Boolean Functions for Dependency Analysis. Technical report, Monash University, 1995.

[CominiLM95] M.Comini, G.Levi, and M.C. Meo. Compositionality of SLD-derivations and their abstractions. In J.Lloyd, editor, Proceedings of the 1995 Int'l Symposium on Logic Programming, pages 561--575. The MIT Press, Cambridge, Mass., 1995.

[CominiLV94] M.Comini, G.Levi, and G.Vitiello. Abstract debugging of logic programs. In L.Fribourg and F.Turini, editors, Proc. Logic Program Synthesis and Transformation and Metaprogramming in Logic 1994, volume 883 of Lecture Notes in Computer Science, pages 440--450. Springer-Verlag, Berlin, 1994.

[CominiLV95a] M.Comini, G.Levi, and G.Vitiello. Declarative diagnosis revisited. In J.Lloyd, editor, Proceedings of the 1995 Int'l Symposium on Logic Programming, pages 275--287. The MIT Press, Cambridge, Mass., 1995.

[CominiLV95] M.Comini, G.Levi, and G.Vitiello. Efficient detection of incompleteness errors in the abstract debugging of logic programs. In M.~Ducass\'{e}, editor, Proc. 2nd International Workshop on Automated and Algorithmic Debugging, AADEBUG'95, 1995.

[CousotC77] P.Cousot and R.Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proc. Fourth ACM Symp. Principles of Programming Languages, pages 238--252, 1977.

[Ferrand87] G.Ferrand. Error Diagnosis in Logic Programming, an Adaptation of E. Y. Shapiro's Method. Journal of Logic Programming, 4:177--198, 1987.

[Ferrand93] G.Ferrand. The notions of symptom and error in declarative diagnosis of logic programs. In P.A. Fritzson, editor, Automated and Algorithmic Debugging, Proc. AADEBUG '93, volume 749 of LNCS, pages 40--57. springer, 1993.

[Lloyd87a] J.W. Lloyd. Declarative error diagnosis. New Generation Computing, 5(2):133--154, 1987.

[Shapiro82] E.Y. Shapiro. Algorithmic program debugging. In Proc. Ninth Annual ACM Symp. on Principles of Programming Languages, pages 412--531. ACM Press, 1982.



Correctness Criteria in Logic program Synthesis
-----------------------------------------------
Yves Deville and Pierre Flener

We define correctness criteria for logic program synthesis. By synthesis, we mean any process that starts from some specification and yields a program. Program construction is thus covered as well. Three levels are considered here. The first level is the intended relation, that is the relation the specifier/programmer has in mind when designing a specification/program. We do not assume any language for defining the intended relation. The second level is the logic specification, that is a formal definition, in logic, of the intended relation. Such logic specifications also cover incomplete specifications. Finally, the third level is the logic program (or any algorithm expressed in logic). Although a fourth level could be considered, namely the executable program, this will not be developped. We thus focus on the logical part of a synthesis process. Correctness criteria relate each of the three levels. This covers many aspects of program synthesis, namely construction from informal specifications, synthesis from complete specifications, synthesis from incomplete specifications, program equivalence, program transformation, and so on. These criteria can be applied even if one of the three levels is missing.



Directional types and abstract interpretation
---------------------------------------------
Jan Malusynski

Directional types express properties of a logic program. The methods for checking directional types presented in the literature turn out to be specialisations of previously known verification methods. We report on a work in progress done in Link\"{o}ping [BM95,Boy96]. Our objectives has been The classical well-typedness conditions are local to the clauses. In our extension the verification conditions consist of a local part and a global non-circularity analysis, similar to that done for attribute grammars. The objective of the presentation is to stimulate discussion about possible relations between checking and inference of directional types and abstract interpretation techniques.

References

[Apt93] K.R. Apt. Declarative programming in Prolog. In Proc. of ILPS'93, pp. 12--35. The MIT Press, 1993.

[Boy96] J. Boye. Directional Types in Logic Programming. Ph.D. thesis, Link{\"o}ping University, 1996.

[BM95] J. Boye and J. Ma{\l}uszy{\'nski. Two aspects of directional types. In Proc.\ of ICLP'95, pp.\ 747--761. The MIT Press, 1995.

[BLR92] F. Bronsard, T. K. Lakshman and U. Reddy. A framework of directionality for proving termination of logic programs. In Proc. of JICSLP'92, pp. 321--335. The MIT Press, 1992.



Specification, validation, and verification of industrially-sized time critical systems in TRIO
------------------------------------------------------------
Angelo Morzenti

TRIO is a temporal logic with metric on time that was defined in recent years at Politecnico di Milano as a formal method for specifying and analyzing time critical systems, and was employed in the development of several industrially-sized applications. We first briefly present the language and then we relate on recent research results, showing two complementary ways of using the specifications to reason about the specified systems: a model-based approach where one considers histories and execution traces to simulate or animate the system, and a more tradiitonal axiomatic approach to infer properties of the system starting from its specification. In the former approach, we defined algorithms for generating finite models of specification formulas to be used for simulation purposes or as test cases. In the latter approach, we defined an axiom system and a calculus for reasoning on TRIO formulas, we used it to construct formal proofs of temporal properties of timed Petri nets, we defined a theory of timed Petri nets refinement, and we are experimenting with the PVS proof checker to automate temporal reasoning with TRIO. Finally, we briefly summarize the results of using TRIO in applied research projects, technology-transfer projects, and purely industrial projects, pointing out the technical, economic and organizational advantages that can be obtained in an industrial setting from a careful and judicious application of formal methods.



Towards proof methods of partial correctness and declarative error diagnosis in (Constraint) Logic Programming.
-----------------------------------------------------------------------
G\'erard Ferrand

We consider correctness of (Constraint) Logic Programs. In fact we consider two dual questions : proof methods of correctness and error diagnosis (debugging).

A great advantage of CLP is its declarative semantics and we consider mainly declarative properties.

LP is a particular case of CLP but some methods cannot be merely adapted from LP to CLP.

On the one hand we study the particular case of logic programs with negation; on the other hand we study CLP in general (without considering negation problem which is not so indispensable). We study new notions which are adapted to CLP, especially concerning incompleteness. Some subtilities are masked in LP because of Independence of Negated Constraints.



The Declarative Side of Magic.
-----------------------------------------------------------------------
Paolo Mascellani and Dino Pedreschi

In this paper, we combine a novel method for proving partial correctness of logic programs with a known method for proving termination, and apply them to the study of the magic-sets transformation. As a result, a declarative reconstruction of efficient bottom-up execution of goal-driven deduction is accomplished, in the sense that the obtained results of partial and total correctness of the transformation abstract away from procedural semantics.



Proving Correctness of CCP and of CLP with dynamic scheduling.
-----------------------------------------------------------------------
F. S. de Boer and M. Gabbrielli
Joint work with E. Marchiori and C. Palamidessi

We develop a compositional proof-system for the partial correctness of concurrent constraint programs. Soundness and (relative) completeness of the system are proved with respect to a denotational semantics based on the notion of strongest postcondition. Completeness is obtained only for a restricted class of ccp programs (confluent ccp). The strongest postcondition semantics provides a justification of the declarative nature of concurrent constraint programs, since it allows to view programs as theories in the specification logic. Previous proof-system is then adapted to obtain a framework for specifying and reasoning about Constraint Logic Programs with dynamic scheduling. The framework consists of a mixed formalism of programs in a ccp-like language, on the one hand, and correctness properties of the logic, on the other hand. In this formalism delay conditions are viewed as a specific class of correctness properties.



From Semantics to Classical Proof Methods by Abstract Interpretation.
-----------------------------------------------------------------------
Patrick Cousot

The process of abstraction, as formalized by abstract interpretation, consists in approximating semantics to obtain specifications of program analysis methods. We show that the same approach can be used to derive classical verification methods from a formal semantics. This is illustrated on discrete transition systems with unbounded nondeterminism by construction of a hierarchy of trace, relational, denotational, predicate transformer and Hoare logics which can all be in natural, demoniac and angelic form. This should clarify some misunderstood points in semantics such as, the almost now forgotten, Scott's thesis (relative to the continuity hupothesis).