[Top] [Contents] [Index] [ ? ]

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

This document was generated by U-leavens-nd\leavens on May, 31 2013 using texi2html