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 条
  • [41] VeyMont: Choreography-Based Generation of Correct Concurrent Programs with Shared Memory
    Rubbens, Robert
    van den Bos, Petra
    Huisman, Marieke
    INTEGRATED FORMAL METHODS, IFM 2024, 2025, 15234 : 217 - 236
  • [42] REACTIVE BEHAVIOR SEMANTICS FOR CONCURRENT CONSTRAINT LOGIC PROGRAMS - (PRELIMINARY VERSION)
    GAIFMAN, H
    MAHER, MJ
    SHAPIRO, E
    LOGIC PROGRAMMING : PROCEEDINGS OF THE NORTH AMERICAN CONFERENCE, 1989, VOL 1-2, 1989, : 553 - 569
  • [43] Proving Programs Continuous
    Zeller, Andreas
    COMMUNICATIONS OF THE ACM, 2012, 55 (08) : 106 - 106
  • [44] PROVING A COMPILER CORRECT - SIMPLE APPROACH
    GERMANO, G
    MAGGIOLOSCHETTINI, A
    JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1975, 10 (03) : 370 - 383
  • [45] PROVING CORRECTNESS OF PROGRAMS
    CONSTABLE, RL
    NOTICES OF THE AMERICAN MATHEMATICAL SOCIETY, 1976, 23 (02): : A334 - A335
  • [46] PROVING CONTROL PROGRAMS
    不详
    ELECTRICAL REVIEW, 1972, 190 (16): : 534 - &
  • [47] Proving Linearizability of Concurrent Queues
    Peng, Jie
    Wen, Tangliu
    Jiang, Dongming
    Journal of Computers (Taiwan), 2024, 35 (05) : 91 - 103
  • [48] CORRECT PROGRAMS
    ALLAN, GJB
    SOFTWARE-PRACTICE & EXPERIENCE, 1983, 13 (08): : 768 - 769
  • [49] Formal verification of concurrent and distributed constraint-based Java']Java programs
    Ramirez, R
    Santosa, AE
    ICECCS 2005: 10TH IEEE INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS, PROCEEDINGS, 2005, : 76 - 84
  • [50] Proving Quicksort Correct in Event-B
    Hallerstede, Stefan
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 259 : 47 - 65
12345