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
    ABADI, M
    LAMPORT, L
    [J]. THEORETICAL COMPUTER SCIENCE, 1991, 82 (02) : 253 - 284
  • [2] ABADI M, 1989, LECT NOTES COMPUT SC, V372, P1
  • [3] DEFINING LIVENESS
    ALPERN, B
    SCHNEIDER, FB
    [J]. INFORMATION PROCESSING LETTERS, 1985, 21 (04) : 181 - 185
  • [4] APPRAISING FAIRNESS IN LANGUAGES FOR DISTRIBUTED-PROGRAMMING
    APT, KR
    FRANCEZ, N
    KATZ, S
    [J]. 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
123