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

[tlaplus] Re: Safety Liveness Decomposition and Machine Closure

When writing real world industrial specs I have indeed never had to worry about the concept of machine closure explicitly. My questions stemmed from a theoretical interest, not a practical one. I was simply curious to know if there were particular, nontrivial examples of non machine closed specifications that were well motivated. Perhaps the "Lazy Caching" spec is the best one to study in this category.

On Thursday, August 13, 2020 at 12:56:36 PM UTC-4 Leslie Lamport wrote:
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/0625daae-9704-4196-9e69-51f71f2090b3n%40googlegroups.com.