Abstract
This paper introduces an alternative operational model for constraint logic programs. First, a transition system is introduced, which is used to define a trace semantics T. Next, an equivalent fixpoint semantics F is defined: a dataflow graph is assigned to a program, and a consequence operator on tuples of sets of constraints is given whose least fixpoint determines one set of constraints for each node of the dataflow graph. To prove that F and T are equivalent, an intermediate semantics O is used, which propagates a given set of constraints through the paths of the dataflow graph. Possible applications of F (and O) are discussed: in particular, its incrementality is used to define a parallel execution model for clp's based on asynchronous processors assigned to the nodes of the program graph. Moreover, O is used to formalize the Intermittent Assertion Method of Burstall [Bur74] for constraint logic programs.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
A. Bossi, M. Gabbrielli, G. Levi, and M. Martelli. The s-semantics approach: theory and applications. The Journal of Logic Programming, 19,29: 149–197, 1994.
R.M. Burstall. Program proving as hand simulation with a little induction. Information Processing, 74:308–312, 1974.
P. Cousot and R. Cousot. “A la Burstall” Intermittent Assertions Induction Principles for Proving Inevitability Properties of Programs. Theoretical Computer Science, 120:123–155, 1993.
L. Colussi and E. Marchiori. Proving correctness of logic programs using axiomatic semantics. In Proceedings of the Eight ICLP, pages 629–644. MIT Press, 1991.
L. Colussi, E. Marchiori and M. Marchiori. On Termination of Constraint Logic Programs. In Proc. First International Conference on Principles and Practice of Constraint Programming. LNCS, Springer-Verlag, 1995. To appear.
W. Drabent and J. Małuszyński. Inductive assertion method for logic programs. TCS, 59(1):133–155, 1988.
P. Deransart and J. Małuszyński. A Grammatical View of Logic Programming. The MIT Press, 1993.
J. Jaffar, S. Michaylov, P.J. Stuckey and R.H.C. Yap. The CLP(R) Language and System. ACM TOPLAS, 14(3):339–395, 1992.
J. Jaffar and M.J. Maher. Constraint Logic Programming: A Survey. JLP 19,20: 503–581, 1994.
K. Kunnen. Signed Data Dependency in Logic Programs. Computer Science Technical Report 719, University of Wisconsin-Madison, 1987.
C. Mellish. Abstract interpretation of Prolog programs. In S. Abramsky and C. Hankin, editors, Abstract Interpretation of declarative languages, pp. 181–198. Ellis Horwood, 1987.
Z. Manna and A. Pnueli. How to cook a proof system for your pet language. In Proceedings 10th Annual ACM Symposium on Principles of Programming Languages (POPL), pp. 141–154, 1983.
U. Nilsson. Systematic semantics approximations of logic programs. In Proc. PLILP, pp. 293–306. Eds. P. Deransart and J. Małuszynski, Springer Verlag, 1990.
C. Stirling. Modal and Temporal Logics. In S. Abramsky, Dov M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, vol-ume 2, pages 477–563, 1992.
B. Wang and R.K. Shyamasundar. A methodology for proving termination of logic programs. JLP 21(1): 1–30, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Colussi, L., Marchiori, E., Marchiori, M. (1995). A dataflow semantics for constraint logic programs. In: Hermenegildo, M., Swierstra, S.D. (eds) Programming Languages: Implementations, Logics and Programs. PLILP 1995. Lecture Notes in Computer Science, vol 982. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0026834
Download citation
DOI: https://doi.org/10.1007/BFb0026834
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60359-7
Online ISBN: 978-3-540-45048-1
eBook Packages: Springer Book Archive