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 条
  • [1] Proving concurrent constraint programs correct
    DeBoer, FS
    Gabbrielli, M
    Marchiori, E
    Palamidessi, C
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1997, 19 (05): : 685 - 725
  • [2] Automatically proving concurrent programs correct
    Cook, Byron
    SEFM 2007: FIFTH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, PROCEEDINGS, 2007, : 269 - 269
  • [3] Proving Concurrent Constraint Programming Correct, Revisited
    Olarte, Carlos
    Pimentel, Elaine
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2015, 312 : 179 - 195
  • [4] Proving correctness of timed concurrent constraint programs
    de Boer, FS
    Gabbrielli, M
    Meo, MC
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, PROCEEDINGS, 2002, 2303 : 37 - 51
  • [5] PROVING PROGRAMS TO BE CORRECT
    KING, JC
    IEEE TRANSACTIONS ON COMPUTERS, 1971, C 20 (11) : 1331 - &
  • [6] PROVING PROGRAMS TO BE CORRECT
    KING, JC
    COMPUTER, 1971, 4 (01) : 44 - &
  • [7] PROVING PROGRAMS CORRECT THROUGH REFINEMENT
    CORRELL, CH
    ACTA INFORMATICA, 1978, 9 (02) : 121 - 132
  • [8] EXERCISE IN PROVING PARALLEL PROGRAMS CORRECT
    GRIES, D
    COMMUNICATIONS OF THE ACM, 1977, 20 (12) : 921 - 930
  • [9] PROVING PROGRAMS CORRECT - ANDERSON,RB
    EVELYN, D
    JOURNAL OF THE OPERATIONAL RESEARCH SOCIETY, 1980, 31 (02) : 198 - 198
  • [10] A formal method for proving programs correct
    Chiang, CC
    Neubart, D
    2001 IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN, AND CYBERNETICS, VOLS 1-5: E-SYSTEMS AND E-MAN FOR CYBERNETICS IN CYBERSPACE, 2002, : 718 - 723
12345