PREDICATE TRANSFORMERS FOR REASONING ABOUT CONCURRENT COMPUTATION

被引:15
|
作者
CHANDY, KM
SANDERS, BA
机构
[1] ETH ZURICH,ETH ZENTRUM,INST COMP SYST,CH-8092 ZURICH,SWITZERLAND
[2] CALTECH,PASADENA,CA 91125
关键词
Concurrent programs - Predicate calculus - Predicate transformers - Reasoning - Sequential programs;
D O I
10.1016/0167-6423(94)00033-B
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
In this paper we propose a calculus for reasoning about concurrent programs inspired by the wp calculus for reasoning about sequential programs. The calculus uses a small set of familiar rules for dealing with safety, progress and parallel composition. A contribution of this paper is to demonstrate how predicate calculus in general, and predicate transformers in particular, can be used to reason about concurrent programs in which fairness plays a critical role.
引用
收藏
页码:129 / 147
页数:19
相关论文
共 50 条
  • [1] Predicate transformers for reasoning about concurrent computation (vol 24, pg 129, 1995)
    Chandy, KM
    Sanders, BA
    SCIENCE OF COMPUTER PROGRAMMING, 1997, 29 (03) : 335 - 335
  • [2] Reasoning about concurrent interaction
    Karlsson, L
    Gustafsson, J
    JOURNAL OF LOGIC AND COMPUTATION, 1999, 9 (05) : 623 - 650
  • [3] Reasoning about effects of concurrent actions
    Baral, C
    Gelfond, M
    JOURNAL OF LOGIC PROGRAMMING, 1997, 31 (1-3): : 85 - 117
  • [4] Underapproximating predicate transformers
    Schmidt, David A.
    STATIC ANALYSIS, PROCEEDINGS, 2006, 4134 : 127 - 143
  • [5] Reasoning about effects of concurrent actions
    Department of Computer Science, University of Texas at El Paso, El Paso, TX 79968, United States
    Journal of Logic Programming, 31 (1-3):
  • [6] Probabilistic predicate transformers
    Morgan, C
    McIver, A
    Seidel, K
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1996, 18 (03): : 325 - 353
  • [7] Predicate/Transition Net Based Model for Reasoning about Actions
    Liu, Yisong
    Zhong, Shan
    Wan, Junpeng
    Wu, Weihua
    PROCEEDINGS OF THE 2008 INTERNATIONAL SYMPOSIUM ON COMPUTATIONAL INTELLIGENCE AND DESIGN, VOL 1, 2008, : 72 - 75
  • [8] REASONING ABOUT PROBABILISTIC BEHAVIOR IN CONCURRENT SYSTEMS
    PURUSHOTHAMAN, S
    SUBRAHMANYAM, PA
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1987, 13 (06) : 740 - 745
  • [9] Reasoning about concurrent systems using types
    Sangiorgi, D
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, 1999, 1578 : 31 - 40
  • [10] Healthiness Conditions for Predicate Transformers
    Keimel, Klaus
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2015, 319 : 255 - 270