Proving Concurrent Constraint Programs Correct

Frank S. De Boer; Maurizio Gabbrielli; Elena Marchiori; Catuscia Palamidessi

doi:10.1145/265943.265954

Proving Concurrent Constraint Programs Correct

Frank S. De Boer
, Maurizio Gabbrielli
, Elena Marchiori
, Catuscia Palamidessi

Research output: Contribution to journal › Article › peer-review

Abstract

We introduce a simple compositional proof system for proving (partial) correctness of concurrentconstraint 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.

Original language	English
Pages (from-to)	685-725
Number of pages	41
Journal	ACM Transactions on Programming Languages and Systems
Volume	19
Issue number	5
DOIs	https://doi.org/10.1145/265943.265954
Publication status	Published - 1 Jan 1997
Externally published	Yes

Keywords

D.1.3 [Programming Techniques]: Concurrent Programming
D.3.1 [Programming Languages]: Formal Definitions and Theory - semantics
F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs - logics of programs

Access to Document

10.1145/265943.265954

Cite this

@article{f94c607345ea4f15b7ecd81d4fc68dea,

title = "Proving Concurrent Constraint Programs Correct",

abstract = "We introduce a simple compositional proof system for proving (partial) correctness of concurrentconstraint 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.",

keywords = "D.1.3 [Programming Techniques]: Concurrent Programming, D.3.1 [Programming Languages]: Formal Definitions and Theory - semantics, F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs - logics of programs",

author = "\{De Boer\}, \{Frank S.\} and Maurizio Gabbrielli and Elena Marchiori and Catuscia Palamidessi",

year = "1997",

month = jan,

day = "1",

doi = "10.1145/265943.265954",

language = "English",

volume = "19",

pages = "685--725",

journal = "ACM Transactions on Programming Languages and Systems",

issn = "0164-0925",

number = "5",

}

TY - JOUR

T1 - Proving Concurrent Constraint Programs Correct

AU - De Boer, Frank S.

AU - Gabbrielli, Maurizio

AU - Marchiori, Elena

AU - Palamidessi, Catuscia

PY - 1997/1/1

Y1 - 1997/1/1

N2 - We introduce a simple compositional proof system for proving (partial) correctness of concurrentconstraint 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.

AB - We introduce a simple compositional proof system for proving (partial) correctness of concurrentconstraint 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.

KW - D.1.3 [Programming Techniques]: Concurrent Programming

KW - D.3.1 [Programming Languages]: Formal Definitions and Theory - semantics

KW - F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs - logics of programs

U2 - 10.1145/265943.265954

DO - 10.1145/265943.265954

M3 - Article

AN - SCOPUS:0031220274

SN - 0164-0925

VL - 19

SP - 685

EP - 725

JO - ACM Transactions on Programming Languages and Systems

JF - ACM Transactions on Programming Languages and Systems

IS - 5

ER -

Proving Concurrent Constraint Programs Correct

Abstract

Keywords

Access to Document

Fingerprint

Cite this