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

[tlaplus] Re: Safety Liveness Decomposition and Machine Closure

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.


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.