The Existence of Refinement Mappings

Refinement mappings are used to prove that a lower-level specification correctly implements a higher-level one. We consider specifications consisting of a state machine (which may be infinite-state) that specifies safety requirements, and an arbitrary supplementary property that specifies liveness requirements. A refinement mapping from a lower-level specification S1 to a higher-level one S2 is a mapping from S1’s state space to S2’s state space. It maps steps of S1’s state machine to steps of S2’s state machine and maps behaviors allowed by S1 to behaviors allowed by S2. We show that, under reasonable assumptions about the specifications, if S1 implements S2, then by adding auxiliary variables to S1 we can guarantee the existence of a refinement mapping. This provides a completeness result for a practical, hierarchical specification method.

The method of proving that one specification implements another by using a refinement mapping was well-established by the mid-80s. (It is clearly described in [54], and it also appears in [50].) It was known that constructing the refinement mapping might require adding history variables to the implementation. Indeed, Lam and Shankar essentially constructed all their refinement mappings with history variables. Jim Saxe discovered a simple example showing that history variables weren’t enough. To handle that example, he devised a more complicated refinement-mapping rule. I realized that I could eliminate that complicated rule, and use ordinary refinement, by introducing a new kind of dummy variable that I called a prophecy variable. A prophecy variable is very much like a history variable, except it predicts the future instead of remembering the past. (Nancy Lynch later rediscovered Saxe’s rule and used it to “simplify” refinement proofs by eliminating prophecy variables.) I then remembered a problematic example by Herlihy and Wing in their classic paper Linearizability: A Correctness Condition for Concurrent Objects that could be handled with prophecy variables.

This paper was my first collaboration with Abadi. Here’s my recollection of how it was written. I had a hunch that history and prophecy variables were all one needed. Abadi had recently joined SRC, and this seemed like a fine opportunity to interest him in the things I was working on. So I described my hunch to him and suggested that he look into proving it. He came back in a few weeks with the results described in the paper. My hunch was right, except that there were hypotheses needed that I hadn’t suspected. Abadi, however, recalls my having had a clearer picture of the final theorem, and that we worked out some of the details together when writing the final proof.

I had just developed the structured proof style described in [101], so I insisted that we write our proofs in this style, which meant rewriting Abadi’s original proofs. In the process, we discovered a number of minor errors in the proofs, but no errors in the results.

This paper won the LICS 1988 Test of Time Award (awarded in 2008).