[tlaplus] Re: Safety Liveness Decomposition and Machine Closure

[Leslie Lamport <tlaplus.ll@xxxxxxxxx>]

There are two kinds of specifications: ones that specify what a system does and those that specify how it does it.  Ideally one writes both and verifies that the how spec implements the what spec.  But currently, I believe that most industrial specs are how specs, and users verify that they satisfy invariants and simple liveness properties.

How specs should be machine closed; if they're not, then they don't really specify how.  In principle, it doesn't matter whether what specs are machine closed.  You should write the spec in a way that makes it easiest to understand.  In practice, machine closed specs are usually easier to understand.  But there are exceptions.  I don't think there's any way to characterize those exceptions.  This is not something to worry about.  You should just make sure that you don't write a non-machine closed spec without realizing that's what you're doing; if you do, then your spec is probably wrong.

Leslie

-- 
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/3119519e-5281-49f4-8ee1-41762e72ac40o%40googlegroups.com.