Composing Specifications

Since the late 80s, I had vague concerns about separating the specification of a system from requirements on the environment. The ability to write specifications as mathematical formulas (first with temporal logic and then, for practical specifications, with TLA) provides an answer. The specification is simply E implies M, where E specifies what we assume of the environment and M specifies what the system guarantees. This specification allows behaviors in which the system violates its guarantee and the environment later violates its assumption–behaviors that no correct implementation could allow. So, we defined the notion of the realizable part of a specification and took as the system specification the realizable part of E implies M. We later decided that introducing an explicit realizable-part operator was a mistake, and that it was better to replace implication with a temporal while operator that made the specifications realizable. That’s the approach we took in [112], which supersedes this paper.

This is the second paper in which we used structured proofs, the first being [92]. In this case, structured proofs were essential to getting the results right. We found reasoning about realizability to be quite tricky, and on several occasions we convinced ourselves of incorrect results, finding the errors only by trying to write structured proofs.