Download ESC/Java2 Implementation Notes

Chapter 3: Status of JML features
43
• \bigint : This is a new type name used in JML to denote an integral type equivalent
to the mathematical integers. That is, it has infinite range and no underflow or overflow
as a result of a fixed bit depth.
Status: The type name is parsed but is equivalent to long.
• \real : This is a new type name used in JML to denote a type equivalent to the mathematical real numbers. That is, it has infinite range and precision and no underflow,
overflow, or rounding error as do float and double.
Status: The type name is parsed but is equivalent to double.
• \LockSet : This type may not be named (there is no token \LockSet). However the
type is implicitly used as the type of the JML token \lockset, as the type of the
argument of \max, and in the LockSet membership operation.
3.16.4 quantified expressions - \forall, \exists, \num of, \max,
\min, \sum, \product
As described in the JML documentation, quantified expressions take the form
( quantifier-keyword type idlist ; range-expr ; expr )
or
( quantifier-keyword type idlist ; ; expr )
or
( quantifier-keyword type idlist ; expr )
The range-expr is a boolean expression; its default value is true. The idlist is a
comma-separated list of identifiers; these are the bound variables of the quantification. No
side-effects are permitted in the predicate or expression.
Status:
• \forall, \exists: Fully implemented and used in static checking.
• \num_of, \max, \min, \sum, \product: Parsed and typechecked but not used in static
checking.
Comment: The keyword \max is used both as a quantifier and as a function. The parser is
able to distinguish the two usages.
3.16.5 Set comprehension
JML has a syntax for expressions whose value is a set. An example is
new JMLObjectSet { Integer i | o.has(i) && i.intValue() > 0 }
No side-effects are permitted in the predicate.