|[Top]||[Contents]||[Index]||[ ? ]|
This is the usual way to declare a specification-only field;
it is also possible to use the
ghost modifier (see section 2.2 Model and Ghost).
Lightweight specifications come from ESC/Java.
JML also has various synonyms for these keywords; one can use
ensures if desired.
See section 9. Method Specifications, for more details.
However, unlike Larch
BISLs and earlier versions of JML, this is not the default for an
assignable clause (see section 9.9.9 Assignable Clauses). Thus
line 9 cannot be omitted without changing the meaning of the
By an identifier, we technically mean an ident in the Java grammar. See section 4.6 Tokens, for details.
Thanks to Patrice Chalin for pushing to define these. Patrice, Joe Kiniry, Peter Müller, Adam Darvas, and David Naumann participated in the initial discussions about what should be in each level.
Thanks to Peter Müller for clarifying this paragraph.
Thanks to Jesus Ravelo for correcting the semantics of measured-by clauses.