Universal extensions to simulate specifications

A previous paper introduced eternity variables as an alternative to the prophecy variables of Abadi and Lamport and proved the formalism to be semantically complete: every simulation F: K → L that preserves quiescence contains a composition of a history extension, an extension with eternity variables, and a refinement mapping. This result is strengthened here in three ways. First, the assumption of preservation of quiescence is eliminated. Second, it is shown that the intermediate extension only depends on K, and is independent of L and F. Third, in order to accommodate implementation relations where the concrete specification (occasionally) does fewer steps than the abstract specification, we weaken the concept of simulation, in such a way that it precisely corresponds to the implementation concept of Abadi and Lamport. We add stuttering history extensions to the repertoire of variable extensions, and show that this extended repertoire suffices to factorize an arbitrary (weakened) simulation. The proofs have been verified with the theorem prover PVS. The methodology of using eternity extensions in correctness proofs is briefly discussed.

Authors

• Wim H. Hesselink

Keywords

• TLA
• Stuttering
• Simulation
• Semantic completeness
• Theorem proving
• Auxiliary variable