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.
No takes yet. Share an insight, caveat, or question.
Abadi et al. (1993) studied this question.
Synapse has enriched 5 related papers. Consider them for comparative context: