Proving concurrent constraint programs correct

ABSTRACT

We introduce a simple compositional proof system for proving (partial) correctness of concurrent constraint programs (CCP). The proof system is based on a denotational approximation of the strongest postcondition semantics of CCP programs. The proof system is proved to be correct for full CCP and complete for the class of programs in which the denotational semantics characterizes exactly the strongest postcondition. This class includes the so-called confluent CCP, a special case of which is constraint logic programming with dynamic scheduling.

REFERENCES

• 1: Krzysztof R. Apt, Formal Justification of a Proof System for Communicating Sequential Processes, Journal of the ACM (JACM), v.30 n.1, p.197-216, Jan. 1983 [doi>10.1145/322358.322372]
• 2: Krzysztof R. Apt , Nissim Francez , Willem P. de Roever, A Proof System for Communicating Sequential Processes, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.3, p.359-385, July 1980 [doi>10.1145/357103.357110]
• 3: Krzysztof R. Apt, Logic programming, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 4: Krzysztof R. Apt, Declarative programming in Prolog, Proceedings of the 1993 international symposium on Logic programming, p.12-35, December 1993, Vancouver, British Columbia, Canada
• 5: Krzysztof R. Apt , Ingrid Luitjes, Verification of Logic Programs with Delay Declarations, Proceedings of the 4th International Conference on Algebraic Methodology and Software Technology, p.66-90, July 03-07, 1995
• 6: Bijan Arbab , Daniel M. Berry, Operational and denotational semantics of prolog, Journal of Logic Programming, v.4 n.4, p.309-329, December 1, 1987 [doi>10.1016/0743-1066(87)90008-2]
• 7: J A Bergstra , J W Klop, Conditional rewrite rules: Confluence and termination, Journal of Computer and System Sciences, v.32 n.3, p.323-362, June 1986 [doi>10.1016/0022-0000(86)90033-4]
• 8: Carlsson, M. 1988. SICStus Prolog user's manual. Tech. Rep., Swedish Institute of Computer Science, Sweden. URL: http://www.sics.se/isl/sicstus.html.
• 9: Michael Codish , Moreno Falaschi , Kim Marriott , William H. Winsborough, Efficient Analysis of Concurrent Constraint Logic Programs, Proceedings of the 20th International Colloquium on Automata, Languages and Programming, p.633-644, July 05-09, 1993
• 10: Colussi, L. and Marchiori, E. 1991. Proving correctness of logic programs using axiomatic semantics. In Proceedings of the 8th International Conference on Logic Programming, K.Furukawa, Ed. The MIT Press, Cambridge, Mass., 629-644.
• 11: Livio Colussi , Elena Marchiori , Massimo Marchiori, A Dataflow Semantics for Constraint Logic Programs, Proceedings of the 7th International Symposium on Programming Languages: Implementations, Logics and Programs, p.431-448, September 20-22, 1995
• 12: Cook, S. 1978. Soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7, 1, 70-90.
• 13: David Gilbert , Catuscia Palamidessi, Concurrent Constraint Programming with Process Mobility, Proceedings of the First International Conference on Computational Logic, p.463-477, July 01, 2000
• 14: De Boer, F. S. and Palamidessi, C. 1990. A fully abstract model of concurrent logic languages. Tech. Rep., Dipartimento di Informatica, Universita diPisa.
• 15: Frank S. de Boer , Alessandra Di Pierro , Catuscia Palamidessi, Nondeterminism and infinite computations in constraint programming, Theoretical Computer Science, v.151 n.1, p.37-78, Nov. 13, 1995
• 16: Frank S. de Boer , Joost N. Kok , Catuscia Palamidessi , Jan J. M. M. Rutten, The Failure of Failures in a Paradigm for Asynchronous Communication, Proceedings of the 2nd International Conference on Concurrency Theory, p.111-126, August 26-29, 1991
• 17: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 18: Falaschi, M., Gabbrielli, M., Marriott, K., and Palamidessi, C. 1993. Compositional analysis for concurrent constraint programming. In Proceedings of the 8th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 210-221.
• 19: M. Falaschi , M. Gabbrielli , K. Marriott , C. Palamidessi, Confluence in Concurrent Constraint Programming, University of Pisa, 1996
• 20: Falaschi, M., Gabbrielli, M., Marriott, K., and Palamidessi, C. 1996b. Constraint logic programming with dynamic scheduling: A semantics based on closure operators. Tech. Rep. 32/96, Dipartimento di Informatica, Univ. di Udine, Italy/ To appear in Information and Computation.
• 21: Ian Foster , Stephen Taylor, Strand: new concepts in parallel programming, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 22: Henkin, L., Monk, J., and Tarski, A. 1971. Cylindric Algebras. Part I and II. North-Holland, Amsterdam.
• 23: Patricia Hill , John Lloyd, The Go¨del programming language, MIT Press, Cambridge, MA, 1994
• 24: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 25: J. Jaffar , J.-L. Lassez, Constraint logic programming, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.111-119, January 21-23, 1987, Munich, West Germany [doi>10.1145/41625.41635]
• 26: Jaffar, J. and Maher, M. J. 1994. Constraint logic programming: A survey. J. Logic Program. 19/20, 503-581.
• 27: Joxan Jaffar , Spiro Michaylov , Peter J. Stuckey , Roland H. C. Yap, The CLP( R ) language and system, ACM Transactions on Programming Languages and Systems (TOPLAS), v.14 n.3, p.339-395, July 1992 [doi>10.1145/129393.129398]
• 28: Jagadeesan, R., Shanbhogue, V., and Saraswat, V. 1991. Angelic non-determinism in concurrent constraint programming. Tech. Rep., System Science Lab., Xerox PARC, Palo Alto, Calif.
• 29: Stefan Lüttringhaus-Kappel, Control generation for logic programs, Proceedings of the tenth international conference on logic programming on Logic programming, p.478-495, August 1993, Budapest, Hungary
• 30: Marchiori, E. and Teusink, F. 1995. Proving termination of logic programs with delay declarations. In Proceedings of the 12th International Logic Programming Symposium,J. Lloyd, Ed. MIT Press, Cambridge, Mass.
• 31: Kim Marriott , María José García de la Banda , Manuel Hermenegildo, Analyzing logic programs with dynamic scheduling, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.240-253, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.177883]
• 32: Naish, L. 1982. An introduction to mu-prolog. Tech. Rep. 82/2, The Univ. of Melbourne, Melbourne, Australia.
• 33: Lee Naish, Negation and control in Prolog, Springer-Verlag New York, Inc., New York, NY, 1986
• 34: Olderog, E. 1991. Nets, Terms and Formulas. Cambridge Tracts in Theoretical Computer Science, Vol. 23. Cambridge University Press, UK.
• 35: Owicki, S. and Gries, D. 1976. An axiomatic proof technique for parallel programs. Acta Inf. 6, 319-340.
• 36: Prakash Panangaden , Vasant Shanbhogue, The expressive power of indeterminate dataflow primitives, Information and Computation, v.98 n.1, p.99-131, May 1992 [doi>10.1016/0890-5401(92)90043-F]
• 37: Prakash Panangaden , Vijay A. Saraswat , P. J. Scott , R. A. G. Seely, A Hyperdoctrinal View of Concurrent Constraint Programming, Proceedings of the REX Workshop on Sematics: Foundations and Applications, p.457-476, June 01-04, 1992
• 38: Plotkin, G. 1980. Dijkstra's predicate transformers and Smyth's powerdomains. Lecture Notes in Computer Science, D. Bjarner, Ed., Vol. 86. Springer-Verlag, Berlin.
• 39: Edmund Robinson, Logical Aspects of Denotational Semantics, Category Theory and Computer Science, p.238-253, September 07-09, 1987
• 40: Vijay A. Saraswat , Martin Rinard, Concurrent constraint programming, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.232-245, December 1989, San Francisco, California, United States [doi>10.1145/96709.96733]
• 41: Vijay Anand Saraswat , Dana S. Scott, Concurrent constraint programming languages, 1989
• 42: Vijay A. Saraswat , Martin Rinard , Prakash Panangaden, The semantic foundations of concurrent constraint programming, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.333-352, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99627]
• 43: Dana S. Scott, Domains for Denotational Semantics, Proceedings of the 9th Colloquium on Automata, Languages and Programming, p.577-613, July 12-16, 1982
• 44: Michael B. Smyth, Power Domains and Predicate Transformers: A Topological View, Proceedings of the 10th Colloquium on Automata, Languages and Programming, p.662-675, July 18-22, 1983
• 45: Wallace, M. and Veron, A. 1993. Two problems - two solutions: One system - ECLiPSe. In Proceedings of the IEEE Col loquium on Advanced Software Technologies for Scheduling.

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs; Pre- and post-conditions
      F.3.2 Semantics of Programming Languages
          Subjects: Denotational semantics

General Terms:
Languages, Theory, Verification

Keywords:
constraint programming, dynamic scheduling, proof theory, strongest postcondition