#65 Update reference manual with jmlspecs-interest decisions

[Gary T. Leavens]

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