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

Universiteit Utrecht
University of Pisa
University of Genoa

Résultats de recherche: Contribution à un journal › Article › Revue par des pairs

Résumé

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.

langue originale	Anglais
Pages (de - à)	685-725
Nombre de pages	41
journal	ACM Transactions on Programming Languages and Systems
Volume	19
Numéro de publication	5
Les DOIs	https://doi.org/10.1145/265943.265954
état	Publié - 1 janv. 1997
Modification externe	Oui

Accès au document

10.1145/265943.265954

Contient cette citation

@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

Résumé

Accès au document

Empreinte digitale

Contient cette citation