The existence of refinement mappings

Martín Abadi, Leslie Lamport
[doi] [Google Scholar] [DBLP] [Citeseer]
Read: 21 October 2019

Theoretical Computer Science 82(2)
Pages 253-284
Topic(s): verification

Theoretical paper justifying the practice of adding auxiliary variables (ghost state) to an implementation to enable refinement proof by providing a completeness proof that a refinement mapping from an implementation S1 to a specification S2 exists if S1 refines S2 and three conditions hold

  • S1 is “machine closed”,
  • S2 has “finite invisible nondeterminism”, and
  • S2 is “internally continuous”.

A refinement mapping is a function from the implementation state (including auxiliary variables) to the specification state. The auxiliary variables can be either “history variables” or “prophecy variables”.