leavens
commented
2 years ago Yes, I'm okay with the statement specification decisions we have made.
The list of type-level specifications seems fine to me.
For model program specifications, extract is correct, as it is a directive to the JML tool to extract a model program specification from the code (see section 4.2 of Sharner, Leavens, Naumann "Modular Verification of Higher-Order Methods
with Mandatory Calls Specified by Model Programs" in OOPSLA’07, October 21–25, 2007, Montréal, Québec, Canada, pp. 351-367, https://doi.org/10.1145/1297027.1297053).
For both model programs and block specifications, the idea of throwing an exception is already handled by the signals clauses in JML specifications, so I don't think that a new kind of clause (throws) is needed. But I am okay with adding throws as a synonym for signals. If we do that, then we should add throws_only.
You are right that I like the "-able" suffixes for assignable and accessible, as well as callable.
It would be fine to deprecate exsures, that was added for compatibility with ESC/Java.
I would not argue for capturable, although that would be logically consistent with my position, it doesn't sound right as an English word. The same holds for divergable.
The working_space and duration keywords were taken from RESOLVE. But I'm okay with alternatives if someone has better ideas.
I would agree to replacing measured_by with decreases (or decreasing).
I'd like to settle on any changes in clause names, in the interests of consistency and intuitiveness. So here is the first of a set of issues on this point.
Loop specs -- separate issue
Statement specs -- Everyone OK with these I presume: assert assume set unreachable refining
Type-level specs-- Also OK I think: invariant axiom represents initially constraint readable...if writable...if monitors_for initializer static_initializer
Model programs: returns, continues, breaks, choose, or , extract -- Gary - should that be extracts instead of extract? -- I think we need to add 'throws'
Block specs, in addition to regular method specs clauses, have: returns, continues, breaks. Also needs 'throws'
Method specs clauses. My preference is for active verbs with consistency across the clauses. Gary likes the connotation of the 'able' suffix. And there is always past experience/backwards compatibility to consider.
requires - OK ensures - OK signals, exsures -- deprecate exsures? 'throws' would be better than signals signals_only -- maybe 'throws_only'? accessible -- I'd prefer 'reads' captures -- OK with me. Does Gary want capturable? callable -- maybe 'calls' ? diverges - OK (anyone proposing 'divergable?) working_space, duration - inconsistent, but no better alternatives and not yet used, so OK measured_by -- OK, but should this be 'decreases' when - OK old - OK, but could be 'let' ('old' is a reminder that it is a pre-state evaluation)
And the biggie: assignable/assigns/modifiable/modifies/writes -- separate issue