#101 Typecheck level 0 JML expressions

[Curtis Clifton]

From the JML Ref Manual:
Some of JML's extensions to Java's expression syntax (see section 11.
Predicates and Specification Expressions), but not all of them, can be
used
at level 0. Note that calls to pure methods and constructors in
spec-expressions are not part of level 0, but are only found at level 1.
We
describe the level 0 specification expressions below.

The result-expression (see section 11.4.1 \result).
The old-expression (see section 11.4.2 \old and \pre).
The fresh-expression (see section 11.4.9 \fresh).
The nonnullelements-expression (see section 11.4.14 \nonnullelements).
The informal-description (see section 11.4.15 Informal Predicates).
The typeof-expression (see section 11.4.16 \typeof).
The elemtype-expression (see section 11.4.17 \elemtype).
The type-expression (see section 11.4.18 \type).
The spec-quantified-expr (see section 11.4.24 Quantified Expressions)
forms
that use the quantifier keywords \forall and \exists (see section
11.4.24.1
Universal and Existential Quantifiers).
(The quantifier keywords \max, \min, \product, and \sum (see section
11.4.24.2 Generalized Quantifiers), as well as \num_of (see section
11.4.24.3 Numerical Quantifier, are all level 1 features.)

The <: operator (see section 11.6.1 Subtype operator).
The <==> and <=!=> operators (see section 11.6.2 Equivalence and
Inequivalence Operators).
The ==> and <== operators (see section 11.6.3 Forward and Reverse
Implication Operators).
The syntax for store-refs (see section 11.7 Store Refs).