Frank S. De Boer
Skip Abstract Section
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.
- Apt, K. 1983. Formal justification of a proof system for communicating sequential processes. J. ACM 30, 197-216.]] Google Scholar
- Apt, K., Francez, N., and de Roever, W. P. 1980. A proof system for communicating sequential processes. ACM Trans. Program. Lang. Syst. 1, 2, 359-385.]] Google Scholar
- Apt, K. R. 1990. Introduction to logic programming. In Handbook of Theoretical Computer Science, J. vanLeeuwen,Ed.,Vol.B:Formal Models and Semantics. Elsevier, Amsterdam and The MIT Press, Cambridge, 495-574.]] Google Scholar
- Apt, K. R.1993. Declarative programming in Prolog. In Proceedings of the International Symposium on Logic Programming, D. Miller, Ed. The MIT Press, Cambridge, Mass.]] Google Scholar
- Apt, K. R. and Luitjes, I. 1995. Verification of logic programs with delay declarations. In Proceedings of the 4th International Conference on Algebraic Methodology and Software Technology (AMAST'95), A. Borzyszkowski and S. Sokolowski, Eds. Lecture Notes in Computer Science. Springer-Verlag, Berlin.]] Google Scholar
- Arbab, B. and Berry, D. 1987. Operational and denotational semantics of Prolog. J. Logic Program. 4, 309-330.]] Google Scholar
- Bergstra, J. and Klop, J. 1986. Conditional rewrite rules: Con uence and termination. J. Comput. Syst. Sci. 32, 323-362.]] Google Scholar
- Carlsson, M. 1988. SICStus Prolog user's manual. Tech. Rep., Swedish Institute of Computer Science, Sweden. URL: http://www.sics.se/isl/sicstus.html.]]Google Scholar
- Codish, M., Fal as chi , M. , Marriott, K., and Winsborough, W. 1993. Efficient analysis of concurrent constraint logic programs. In Proceedings of the 20th International Col loquium on Automata, Languages, and Programming, A. Lingas, R. Karlsson, and S. Carlsson, Eds. Lecture Notes in Computer Science, Vol. 700. Springer-Verlag, Berlin, 633-644.]] Google Scholar
- 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.]]Google Scholar
- Colussi, L., Marchiori, E., and Marchiori, M. 1995. A data ow semantics for constraint logic programs. In Proceedings of the 7th International Symposium on Programming Languages, Implementations, Logics and Programs, M. Hermenegildo and S. D. Swierstra, Eds. Springer Verlag.]] Google Scholar
- Cook, S. 1978. Soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7, 1, 70-90.]]Google Scholar
- De Boer, F. and Palamidessi, C. 1992. A process algebra for concurrent constraint programming. In Proceedings of the Joint International Conference and Symposium on Logic Programming, K. Apt, Ed. Series in Logic Programming. The MIT Press, Cambridge, Mass, 463-477.]] Google Scholar
- De Boer, F. S. and Palamidessi, C. 1990. A fully abstract model of concurrent logic languages. Tech. Rep., Dipartimento di Informatica, Universita diPisa.]]Google Scholar
- De Boer, F. S., di Pierro, A., and Palamidessi, C. 1995. Infinite computations in nondeterministic constraint programming. Theor. Comput. Sci. 151, 37-78.]] Google Scholar
- De Boer, F. S., Kok, J. N., Palamidessi, C., and Rutten, J. J. M. M. 1991. The failure of failures: Towards a paradigm for asynchronous communication. In Proceedings of Concur '91. Lecture Notes in Computer Science, Vol. 527. Springer-Verlag, Berlin.]] Google Scholar
- Dijkstra, E. 1976. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, N.J.]] Google Scholar
- 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.]]Google Scholar
- Falaschi, M., Gabbrielli, M., Marriott, K., and Palamidessi, C. 1996a. Con uence in concurrent constraint programming. Tech. Rep. 96/284, Dept. of Computer Science, Monash University, Australia. To appear in Theoretical Computer Science.]] Google Scholar
- 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.]]Google Scholar
- Foster, I. and Taylor, S. 1989. Strand: New Concepts in Parallel Programming. Prentice Hall, Englewood Cliffs, N.J.]] Google Scholar
- Henkin, L., Monk, J., and Tarski, A. 1971. Cylindric Algebras. Part I and II. North-Holland, Amsterdam.]]Google Scholar
- Hill, P. M. and Lloyd, J. W. 1994. The G'odel Programming Language. TheMITPress, Cambridge, Mass.]] Google Scholar
- Hoare, C. 1969. An axiomatic basis for computer programming. Commun. ACM 12, 10, 576-580.]] Google Scholar
- Jaffar, J. and Lassez, J.-L. 1987. Constraint logic programming. In Proceedings of the 14th Annual ACM Symposium on Principles of Programming Languages. ACM Press, New York, 111-119.]] Google Scholar
- Jaffar, J. and Maher, M. J. 1994. Constraint logic programming: A survey. J. Logic Program. 19/20, 503-581.]]Google Scholar
- Jaffar, J., Michayov, S., Stuckey, P. J., and Yap, R. H. C. 1992. The CLP( R ) language and system. ACM Trans. Program. Lang. Syst. 14, 3 (July), 339-395.]] Google Scholar
- 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.]]Google Scholar
- Luttringhaus-Kappel, S. 1993. Control generation for logic programs. In Proceedings of the 10th International Conference on Logic Programming, D. Warren, Ed. MIT Press, Cambridge, Mass., 478-495.]] Google Scholar
- 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.]]Google Scholar
- Marriott, K., de la Banda, M. G., and Hermenegildo, M. 1994. Analyzing logic programs with dynamic scheduling. In Proceedings of the 21st Annual ACM Symposium on Principles of Programming Languages. ACM Press, New York, 240-253.]] Google Scholar
- Naish, L. 1982. An introduction to mu-prolog. Tech. Rep. 82/2, The Univ. of Melbourne, Melbourne, Australia.]]Google Scholar
- Naish, L. 1986. Negation and Control in Prolog. Lecture Notes in Computer Science, Vol. 238. Springer-Verlag, Berlin.]] Google Scholar
- Olderog, E. 1991. Nets, Terms and Formulas. Cambridge Tracts in Theoretical Computer Science, Vol. 23. Cambridge University Press, UK.]] Google Scholar
- Owicki, S. and Gries, D. 1976. An axiomatic proof technique for parallel programs. Acta Inf. 6, 319-340.]]Google Scholar
- Panangaden, P. and Shanbhogue, V. 1992. The expressive power of indeterminate data ow primitives. Inf. Comput. 98, 1, 99-131, 1992.]] Google Scholar
- Panangaden, P., Saraswat, V., Scott, P., and Seely, R. 1992. A hyperdoctrinal view of concurrent constraint programming. In In Proceedings of the REX Workshop. Lecture Notes in Computer Science, Vol. 666. Springer-Verlag, Berlin, 457-476.]] Google Scholar
- Plotkin, G. 1980. Dijkstra's predicate transformers and Smyth's powerdomains. Lecture Notes in Computer Science, D. Bjarner, Ed., Vol. 86. Springer-Verlag, Berlin.]] Google Scholar
- Robinson, E. 1987. Logical aspects of denotational semantics. Lecture Notes in Computer Science, D.H. Pitt, A. Poigne, and D.E. Rydeheard, Eds., Vol. 283. Springer-Verlag, Berlin.]] Google Scholar
- Saraswat, V. and Rinard, M. 1990. Concurrent constraint programming. In Proceedings of the 17th ACM Symposium on Principles of Programming Languages. ACM Press, New York, 232-245.]] Google Scholar
- Saraswat, V. A.1989. Concurrent constraint programming languages. Ph.D. thesis, Carnegie- Mellon Univ., Pittsburgh, Pa. Also in ACM distinguished dissertation series. The MIT Press, 1993.]] Google Scholar
- Saraswat, V. A., Rinard, M., and Panangaden, P. 1991. Semantic foundation of concurrent constraint programming. In Proceedings of the 18th Annual ACM Symposium on Principles of Programming Languages. ACM Press, New York, 333-353.]] Google Scholar
- Scott, D. 1982. Domains for denotational semantics. In Proceedings of the 9th International Conference on Automata, Languages and Programming,M. NielsenandE. M. Schmidt,Eds. Lecture Notes in Computer Science, Vol. 140. Springer-Verlag, Berlin, 577-613.]] Google Scholar
- Smyth, M. 1983. Powerdomains and predicate transformers: A topological view. In Proceedings of the International Conference on Automata, Languages and Programming. Lecture Notes in Computer Science, Vol. 154. Springer-Verlag, Berlin, 662-675.]] Google Scholar
- 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.]]Google Scholar
Index Terms
- Proving concurrent constraint programs correct
Recommendations
Proving concurrent constraint programs correct
POPL '94: Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languagesWe 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 ...
Eliminability of cut in hypersequent calculi for some modal logics of linear frames
Hypersequent calculus HC for three modal logics of linear frames (K4.3, KD4.3 and S4.3) is presented.Adequacy of HC for these logics is shown.Eliminability of Cut is demonstrated. Hypersequent calculi, introduced independently by Pottinger and Avron, ...
Completeness and Cut-elimination in the Intuitionistic Theory of Types
In this paper we define a model theory and give a semantic proof of cut-elimination for ICTT, an intuitionistic formulation of Church's theory of types defined by Miller et al. and the basis for the λProlog programming language. Our approach, extending ...
Comments