Hi everyone. Refinement is a big part of TLA+. Pretty much all examples that I've seen of TLA+ refinement are of the following form:
Impl => Spec
where Impl is the specification of an implementation, and Spec is a higher-level specification. The intuition of this is that Impl must have a subset of Spec's behaviors in order to be true, i.e. Spec can "do more" and Impl can "do less."
My first question is, why don't I see the opposite statement being checked? That is:
Spec => Impl
Is this not also an acceptable correctness statement, even though it has different properties?
That's where my question about the relation to simulation comes in. Is it accurate to say that the first refinement shown here is equivalent to a backward simulation and the second is a forward simulation? If not, what are the differences?
For background, the reason I've become curious to understand this better is that I've been reading and re-reading
A formally verified compiler back-end, the paper about proving compiler correctness in CompCert. While the verification of CompCert doesn't use TLA+, and that might lead to a difference in terminology, in the paper they equate backward simulation to refinement. To verify the compiler, however, they chose to prove forward simulation, which has me wondering why we don't prove more TLA+ specifications via Spec => Impl.
Most of all I'm just looking for a clarification of terminology and some deeper intuition about refinement and simulation. Thanks for any responses.
- Alex Weisberger