Download ESC/Java2 Implementation Notes

Chapter 3: Status of JML features
45
3.17.1 [ ident | super | this ] . [ ident | this ]
This designates a field of an object.
Status: Implemented within modifies clauses.
3.17.2 [ ident | super | this ] .*
This designates all static and instance fields, of any privacy level, including those inherited
from superclasses and interfaces, of the given object.
Status: Not implemented.
3.17.3 [ ident | super | this ] [expr ]
This designates an element of the given array object.
Status: Implemented within modifies clauses.
3.17.4 [ ident | super | this ] [expr..expr2 ]
This designates a range of elements of the given array object.
Status: Not implemented.
3.17.5 [ ident | super | this ] [*]
This designates all the elements of the given array object.
Status: Not implemented.
3.17.6 classname.*
This designates all static fields, of any privacy level, including those in superclasses and
interfaces, and including ghost and model fields, of the given class.
Status: Not implemented.
3.17.7 \nothing
This designates an empty set of store-refs. It may be used with the modifies, accessible,
and callable clauses. If \nothing appears in a sequence of other store-refs, it is ignored,
since a sequence of store-refs is essentially a union.
Status: Fully implemented.
3.17.8 \everything
This designates a universal set - the set of references to all object and class fields for every
object and class allocated in the current state of the program. It may be used with the
modifies, accessible, and callable clauses.
Status: Fully parsed - refer to the clause descriptions for specific behavior.