COMPOSING SPECIFICATIONS

被引：203

作者：

ABADI, M

LAMPORT, L

机构：

[1] Systems Research Center, Digital Equipment Corporation, Palo Alto, CA 94301

来源：

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS | 1993年 / 15卷 / 01期

关键词：

COMPOSITIONALITY; CONCURRENT PROGRAMMING; LIVENESS PROPERTIES; MODULAR SPECIFICATION; SAFETY PROPERTIES;

D O I：

10.1145/151646.151649

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

A rigorous modular specification method requires a proof rule asserting that if each component behaves correctly in isolation, then it behave correctly in concert with other components. Such a rule is subtle because a component need behave correctly only when its environment does, and each component is part of the others' environments. We examine the precise distinction between a system and its environment, and provide the requisite proof rule when module 8 are specified with safety and liveness properties.

引用

页码：73 / 132

页数：60

共 28 条

[1] THE EXISTENCE OF REFINEMENT MAPPINGS [J].

ABADI, M ;

LAMPORT, L .

THEORETICAL COMPUTER SCIENCE, 1991, 82 (02) :253-284

[2]

ABADI M, 1989, LECT NOTES COMPUT SC, V372, P1

[3] DEFINING LIVENESS [J].

ALPERN, B ;

SCHNEIDER, FB .

INFORMATION PROCESSING LETTERS, 1985, 21 (04) :181-185

[4] APPRAISING FAIRNESS IN LANGUAGES FOR DISTRIBUTED-PROGRAMMING [J].

APT, KR ;

FRANCEZ, N ;

KATZ, S .

DISTRIBUTED COMPUTING, 1988, 2 (04) :226-241

[5]

BARRINGER H, 1986, 18TH POPL ACM, P173

[6]

BROY M, 1991, 3RD WORKSH CONC COMP, V191, P47

[7]

DILL DL, 1988, THESIS CARNEGIEMELLO

[8]

HAREL D, 1985, NATO ASI SERIES F, V13, P477

[9]

Hoare C. A. R., 1972, Acta Informatica, V1, P271, DOI 10.1007/BF00289507

[10]

Hoare C. A. R., 1985, COMMUNICATING SEQUEN

← 1 2 3 →