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.
Leslie