[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] TLA+-style Refinement vs. Backward and Forward Simulation

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

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAEPrOmK8gX76ujwJ5-_Go0Uwz0q4LFG4vMSyPOqwLi%2BWhfMwjw%40mail.gmail.com.