#119 Allow all specification constructs in model methods

[Gary T. Leavens]

A model method in JML is necessarily found in an
annotation. As such, a model method should be able to
access ghost fields and model fields. This would allow,
in many cases, more succinct writing of model methods.
It would also make the bodies of model methods more
consistent and regular with other annotation contexts
(assertions, model programs) where model field and
ghost field access is allowed.

A potential drawback of allowing model field access in
model methods is the possibility of infinite recursions
when a model field access calls involves a represents
clause that calls back to the original model method. It's
not clear how often this would happen or how hard it
would be to understand.

This item was suggested to me by Clyde Ruby.

[Gary T. Leavens]

Logged In: YES
user_id=633675

The jmlspecs-interest group has agreed that we should
generalize this a bit, to allow use of all JML specification
expressions in model methods (see that group's email of 27
Jun 2005).

That would subsume this change, but I'm adding those
changes here underneath that, as part of it.