Footnotes

(1)

Note that JML annotations are not the same as Java (5) annotations. The at-sign (@) at the start of a JML annotation comment is not part of the keyword, such as pure used in JML, but is used to distinguish Java comments from JML annotations and must be adjacent to the /* or // in such a JML annotation comment.

(2)

For historical reasons, JML also allows one to use modifiable and modifies as synonyms for assignable.