An experiment in program composition and proof

被引：13

作者：

Chandy, KM ^{[1
]}

Charpentier, M ^{[1
]}

机构：

[1] CALTECH, Dept Comp Sci, Pasadena, CA 91125 USA

来源：

FORMAL METHODS IN SYSTEM DESIGN | 2002年 / 20卷 / 01期

关键词：

composition; formal specification; program verification; temporal logic; UNITY;

D O I：

10.1023/A:1012952311559

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

This paper explores a compositional approach to program specification, development and proof. We apply a theory of composition to a problem in distributed computing with the goal of understanding the strengths and weaknesses of this compositional approach. First, we describe the theory briefly. Then we give a specification of a desired system. Next, we propose a design of the desired system as a composition of components and prove its correctness. Finally, we show how the proof can be reused for a slightly different compositional structure by using the concept of observation.

引用

页码：7 / 21

页数：15

共 17 条

[1] Abrial J., 2005, The B-book: Assigning Programs to Meanings
[2] PREDICATE TRANSFORMERS FOR REASONING ABOUT CONCURRENT COMPUTATION
CHANDY, KM
SANDERS, BA
[J]. SCIENCE OF COMPUTER PROGRAMMING, 1995, 24 (02) : 129 - 147
[3] CHANDY KM, 1996, 96035 U FLOR DEP COM
[4] CHANDY KM, 1988, PARALLEL PROGRAM DES
[5] Charpentier M, 1998, LECT NOTES COMPUT SC, V1388, P820
[6] CHARPENTIER M, 1999, CSTR9902 CALTECH, P29
[7] CHARPENTIER M, 1999, LECT NOTES COMPUTER, V1586, P1215
[8] CHARPENTIER M, 1997, THESIS I NATL POLYTE
[9] MODEL CHECKING AND MODULAR VERIFICATION
GRUMBERG, O
LONG, DE
[J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1994, 16 (03): : 843 - 871
[10] THE TEMPORAL LOGIC OF ACTIONS
LAMPORT, L
[J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1994, 16 (03): : 872 - 923

← 1 2 →