Composing specifications
- 1 January 1993
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems
- Vol. 15 (1), 73-132
- https://doi.org/10.1145/151646.151649
Abstract
A rigorous modular specification method requires a proof rule asserting that if each component behaves correctly in isolation, then it behaves 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 modules are specified with safety and liveness properties.Keywords
This publication has 14 references indexed in Scilit:
- The existence of refinement mappingsTheoretical Computer Science, 1991
- A simple approach to specifying concurrent systemsCommunications of the ACM, 1989
- Trace Theory for Automatic Hierarchical Verification of Speed-Independent CircuitsPublished by MIT Press ,1989
- Appraising fairness in languages for distributed programmingDistributed Computing, 1988
- Defining livenessInformation Processing Letters, 1985
- On the Development of Reactive SystemsPublished by Springer Nature ,1985
- The ``Hoare Logic'' of CSP, and All ThatACM Transactions on Programming Languages and Systems, 1984
- Specifying Concurrent Program ModulesACM Transactions on Programming Languages and Systems, 1983
- A Calculus of Communicating SystemsLecture Notes in Computer Science, 1980
- Proof of correctness of data representationsActa Informatica, 1972