----------------------------------------------------------

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.

---------------------------------------------

Livio Colussi

- the incrementality of F is used to define a parallel execution model for clp's based on asyncrhronous processors assigned to the nodes of the data flow graph,
- O is used to formalize the Intermittent Assertions Method of Burstall for clp's.
- O can be used to develop formal methods for reasoning about run-time properties of clp's: as an example, a necessary and sufficient condition for termination of clp's is obtained and a sufficient termination criterion is given.

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.

----------------------------------------------------------

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.

-----------------------------------------------

Yves Deville and Pierre Flener

---------------------------------------------

Jan Malusynski

- to extend the well-typedness condition used commonly in the literature, (see e.g.[Apt93,BLR92]),
- to relate our extension [BM95] to these well-typedness conditions, and to more general verification methods,
- to discuss the feasibility of automatic type checking and type inference and to implement a prototype type-checker [Boy96].

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.

------------------------------------------------------------

Angelo Morzenti

-----------------------------------------------------------------------

G\'erard Ferrand

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.

-----------------------------------------------------------------------

Paolo Mascellani and Dino Pedreschi

-----------------------------------------------------------------------

F. S. de Boer and M. Gabbrielli

Joint work with E. Marchiori and C. Palamidessi

-----------------------------------------------------------------------

Patrick Cousot