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

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

Spec describes those behaviors that are considered correct.  Impl describes those behaviors that the system can produce.  The engineers I talk to want to know that every behavior the system can produce is correct, for which they have to check if Impl => Spec is true.  I presume that for compiler verification, Spec describes the code written in the compiler's input language and Impl describes the compiled code.  I have no idea why they want to verify Spec => Impl.  Can you explain why they want to do that?


On Friday, March 4, 2022 at 8:08:43 PM UTC-8 alex.m.w...@xxxxxxxxx wrote:
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/0a1c743a-7e19-4439-965f-fd11405bf4afn%40googlegroups.com.