The following need to be recorded in the reference
manual.
Decided that specification expressions in JML (and
quantifiers in
particular) should not be garbage-sensitive (4 May
2005, 12 May
2005), and thus that we should not add a \allocated
primitive to JML
(13 May 2005).
We disallow final model fields, as it's better to use a
final ghost
field, which can be initialized (10 May 2005). (This is
already
implemented in the ISU JML tools, but we reaffirmed
this decision.)