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

来源：

SCIENCE OF COMPUTER PROGRAMMING | 1995年 / 24卷 / 02期

关键词：

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

共 12 条

[1] CHANDY KM, 1993, FORMAL ASPECTS COMPU
[2] CHANDY KM, 1988, PARALLEL PROGRAM DES
[3] Dijkstra E.W, 1990, PREDICATE CALCULUS P
[4] Dijkstra EW, 1976, DISCIPLINE PROGRAMMI
[5] GOLDSCHLAG D, 1992, THESIS U TEXAS AUSTI
[6] TENTATIVE STEPS TOWARD A DEVELOPMENT METHOD FOR INTERFERING PROGRAMS
JONES, CB
[J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1983, 5 (04): : 596 - 619
[7] JUTLA CS, 1989, 8TH P ACM S PRINC DI
[8] A PREDICATE TRANSFORMER FOR PROGRESS
KNAPP, E
[J]. INFORMATION PROCESSING LETTERS, 1990, 33 (06) : 323 - 330
[9] THE TEMPORAL LOGIC OF ACTIONS
LAMPORT, L
[J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1994, 16 (03): : 872 - 923
[10] LAMPORT L, 1990, ACM T PROG LANG SYS, V12

← 1 2 →