Footnotes

(1)

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

(2)

Lightweight specifications come from ESC/Java.

(3)

JML also has various synonyms for these keywords; one can use pre for requires, modifies or modifiable for assignable, and post for ensures, if desired. See section 9. Method Specifications, for more details.

(4)

However, unlike Larch BISLs and earlier versions of JML, this is not the default for an omitted assignable clause (see section 9.9.9 Assignable Clauses). Thus line 9 cannot be omitted without changing the meaning of the specification.

(5)

By an identifier, we technically mean an ident in the Java grammar. See section 4.6 Tokens, for details.

(6)

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.

(7)

Thanks to Peter Müller for clarifying this paragraph.

(8)

Thanks to Jesus Ravelo for correcting the semantics of measured-by clauses.