|[Top]||[Contents]||[Index]||[ ? ]|
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
// in such a JML annotation comment.
For historical reasons, JML also allows one to use
modifies as synonyms for