Proving concurrent constraint programs correct

被引：0
|
作者：
Universiteit Utrecht, Utrecht, Netherlands [1 ]
机构：
来源：
ACM Trans Program Lang Syst | / 5卷 / 685-725期
关键词：
Computational linguistics - Constraint theory - Logic programming - Theorem proving;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
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.
引用
收藏
相关论文
共 50 条
  • [21] Automatic verification of timed concurrent constraint programs
    Falaschi, Moreno
    Villanueva, Alicia
    THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2006, 6 : 265 - 300
  • [22] Demand transformation analysis for concurrent constraint programs
    Falaschi, M
    Hicks, P
    Winsborough, W
    JOURNAL OF LOGIC PROGRAMMING, 2000, 42 (03): : 185 - 215
  • [23] Abstract diagnosis for timed concurrent constraint programs
    Comini, Marco
    Titolo, Laura
    Villanueva, Alicia
    THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2011, 11 : 487 - 502
  • [24] Abstract interpretation of temporal concurrent constraint programs
    Falaschi, Moreno
    Olarte, Carlos
    Palamidessi, Catuscia
    Theory and Practice of Logic Programming, 2015, 15 (03) : 312 - 357
  • [25] Abstract interpretation of temporal concurrent constraint programs
    Falaschi, Moreno
    Olarte, Carlos
    Palamidessi, Catuscia
    THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2015, 15 : 312 - 357
  • [26] Declarative diagnosis of temporal concurrent constraint programs
    Falaschi, M.
    Olarte, C.
    Palamidessi, C.
    Valencia, F.
    LOGIC PROGRAMMING, PROCEEDINGS, 2007, 4670 : 271 - +
  • [27] Phase semantics and verification of concurrent constraint programs
    Fages, F
    Ruet, P
    Soliman, S
    THIRTEENTH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 1998, : 141 - 152
  • [28] A Framework for Abstract Interpretation of Timed Concurrent Constraint Programs
    Falaschi, Moreno
    Olarte, Carlos
    Palamidessi, Catuscia
    PPDP'09: PROCEEDINGS OF THE 11TH INTERNATIONAL ACM SIGPLAN SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING, 2009, : 207 - 217
  • [29] UNFOLDING AND FIXPOINT SEMANTICS OF CONCURRENT CONSTRAINT LOGIC PROGRAMS
    GABBRIELLI, M
    LEVI, G
    LECTURE NOTES IN COMPUTER SCIENCE, 1990, 463 : 204 - 216
  • [30] UNFOLDING AND FIXPOINT SEMANTICS OF CONCURRENT CONSTRAINT LOGIC PROGRAMS
    GABBRIELLI, M
    LEVI, G
    THEORETICAL COMPUTER SCIENCE, 1992, 105 (01) : 85 - 128
12345