3. Extensions to Java Expressions

JML makes extensions to the Java expression syntax for two purposes. The main set of extensions are used in predicates. But there are also some extensions used in store-refs, which are themselves used in the assignable and represents clauses.

We give an overview of these extensions in this section. However, we only describe the most important and useful extensions here. See the JML Reference Manual [Leavens-etal-JMLRef] for more extensions and for more detail.

3.1 Extensions to Java Expressions for Predicates
3.2 Extensions to Java Expressions for Store-Refs

3.1 Extensions to Java Expressions for Predicates

The expressions that can be used as predicates in JML are an extension to the side-effect free Java expressions. Since predicates are required to be side-effect free, the following Java operators are not allowed within predicates:

• assignment (=), and the various assignment operators (such as +=, -=, etc.)

• all forms of increment and decrement operators (++ and --),

• calls to methods that are not pure, and

• any use of operator new that would call a constructor that is not pure.

Furthermore, within method specifications that are not model programs, one cannot use super to call a pure superclass method, because it is confusing in combination with JML's specification inheritance.(26)

We allow the allocation of storage (e.g., using operator new and pure constructors) in predicates, because such storage can never be referred to after the evaluation of the predicate, and because such pure constructors have no side-effects other than initializing the new objects so created.

JML adds the following new syntax to the Java expression syntax, for use in predicates (see the JML Reference Manual [Leavens-etal-JMLRef] for syntactic details such as precedence):

• Informal descriptions, which look like

  (* some text describing a Boolean-valued predicate *)

  have type boolean. Their meaning is either true or false, but is entirely determined by the reader. Since informal descriptions are not-executable, they may be treated differently by different tools in different situations.

• ==> and <== for logical implication and reverse implication. For example, the formula raining ==> getsWet is true if either raining is false or getsWet is true. The formula getsWet <== raining means the same thing. The ==> operator associates to the right, but the <== operator associates to the left. The expressions on both sides of these operators must be of type boolean, and the type of the result is also boolean.

• <==> and <=!=> for logical equivalence and logical inequivalence, respectively. The expressions on either side of these operators must be of type boolean, and the type of the result is also boolean. Note that <==> means the same thing as == for expressions of type boolean, and <=!=> means the same thing as != for boolean expressions; however, <==> and <=!=> have a much lower precedence, and are also associative and symmetric.

• \forall and \exists, which are universal and existential quantifiers (respectively); for example,

  (\forall int i,j; 0 <= i && i < j && j < 10; a[i] < a[j])

  says that a is sorted at indexes between 0 and 9. The quantifiers range over all potential values of the variables declared which satisfy the range predicate, given between the semicolons (;). If the range predicate is omitted, it defaults to true. Since a quantifier quantifies over all potential values of the variables, when the variables declared are reference types, they may be null, or may refer to objects not constructed by the program; one should use a range predicate to eliminate such cases if they are not desired. The type of a universal and existential quantifier is boolean.

• \max, \min, \product, and \sum, which are generalized quantifiers that return the maximum, minimum, product, or sum of the values of the expressions given, where the variables satisfy the given range. The range predicate must be of type boolean. The expression in the body must be a built-in numeric type, such as int or double; the type of the quantified expression as a whole is the type of its body. The body of a quantified expression is the last top-level expression it contains; it is the expression following the range predicate, if there is one. As with the universal and existential quantifiers, if the range predicate is omitted, it defaults to true. For example, the following equations are all true (see chapter 3 of [Cohen90]):

  (\sum int i; 0 <= i && i < 5; i) == 0 + 1 + 2 + 3 + 4 (\product int i; 0 < i && i < 5; i) == 1 * 2 * 3 * 4 (\max int i; 0 <= i && i < 5; i) == 4 (\min int i; 0 <= i && i < 5; i-1) == -1

  For computing the value of a sum or product, Java's arithmetic is used. The meaning thus depends on the type of the expression. For example, in Java, floating point numbers use the IEEE 754 standard, and thus when an overflow occurs, the appropriate positive or negative infinity is returned. However, Java integers wrap on overflow. Consider the following examples.

  (\product float f; 1.0e30f < f && f < 1.0e38f; f) == Float.POSITIVE_INFINITY (\sum int i; i == Integer.MAX_VALUE || i == 1; i) == Integer.MAX_VALUE + 1 == Integer.MIN_VALUE

  When the range predicate is not satisfiable, the sum is 0 and the product is 1; for example:

  (\sum int i; false; i) == 0 (\product double d; false; d*d) == 1.0

  When the range predicate is not satisfiable for \max the result is the smallest number with the type of the expression in the body; for floating point numbers, negative infinity is used. Similarly, when the range predicate is not satisfiable for \min, the result is the largest number with the type of the expression in the body.

• \num_of, which is "numerical quantifier." It returns the number of values for its variables for which the range and the expression in its body are true. Both the range predicate and the body must have type boolean, and the entire quantified expression has type long. The meaning of this quantifier is defined by the following equation (see p. 57 of [Cohen90]).

  (\num_of T x; R(x); P(x)) == (\sum T x; R(x) && P(x); 1L)

• Set comprehensions, which can be used to succinctly define sets; for example, the following is the JMLObjectSet that is the subset of non-null Integer objects found in the set myIntSet whose values are between 0 and 10, inclusive.

  new JMLObjectSet {Integer i | myIntSet.has(i) && i != null && 0 <= i.getInteger() && i.getInteger() <= 10 }

  The syntax of JML (see the JML Reference Manual [Leavens-etal-JMLRef] for details) limits set comprehensions so that following the vertical bar (`|') is always an invocation of the has method of some set on the variable declared. (This restriction is used to avoid Russell's paradox [Whitehead-Russell25].) In practice, one either starts from some relevant set at hand, or one can start from the sets containing the objects of primitive types found in org.jmlspecs.models.JMLModelObjectSet and (in the same Java package) JMLModelValueSet. The type of such an expression is the type named following new, which must be JMLObjectSet or JMLValueSet.

• \elemtype, which returns the most-specific static type shared by all elements of its array argument [Leino-Nelson-Saxe00]. For example, \elemtype(\type(int[])) is \type(int). The argument to \elemtype must be an expression of type \TYPE, which JML considers to be the same as java.lang.Class, and its result also has type \TYPE. If the argument is not an array type, the result is null.

• \fresh, which asserts that objects were freshly allocated; for example, \fresh(x,y) asserts that x and y are not null and that the objects bound to these identifiers were not allocated in the pre-state. The arguments to \fresh can have any reference type, and the type of the overall expression is boolean.(27)

• \nonnullelements, which can be used to assert that an array and its elements are all non-null. For example, \nonnullelements(myArray), is equivalent to [Leino-Nelson-Saxe00]

  myArray != null && (\forall int i; 0 <= i && i < myArray.length; myArray[i] != null)

• \old, which can be used to refer to values in the pre-state; e.g., \old(myPoint.x) is the value of the x field of the object myPoint in the pre-state. The type of such an expression is the type of the expression it contains; for example the type of \old(myPoint.x) is the type of myPoint.x. The keyword \old can only be used in an ensures-clause, a signals-clause, or a history-constraint; it cannot be used, for example, in preconditions.

• \result, which, in an ensures clause is the value or object that is being returned by a method. Its type is the return type of the method; hence it is a type error to use \result in a void method or in a constructor. The keyword \result can only be used in an ensures-clause; it cannot be used, for example, in preconditions or in signals clauses.

• \typeof, which returns the most-specific dynamic type of an expression's value [Leino-Nelson-Saxe00]. The meaning of \typeof(E) is unspecified if E is null. If E has a static type that is a reference type, then \typeof(E) means the same thing as E.getClass(). For example, if c is a variable of static type Collection that holds an object of class HashSet, then \typeof(c) is HashSet.class, which is the same thing as \type(HashSet). If E has a static type that is not a reference type, then \typeof(E) means the instance of java.lang.Class that represents its static type. For example, \typeof(true) is Boolean.TYPE, which is the same as \type(boolean). Thus an expression of the form \typeof(E) has type \TYPE, which JML considers to be the same as java.lang.Class.

• <:, which compares two reference types and returns true when the type on the left is a subtype of the type on the right [Leino-Nelson-Saxe00]. Although the notation might suggest otherwise, this operator is also reflexive; a type will compare as <: with itself. In an expression of the form E1 <: E2, both E1 and E2 must have type \TYPE; since in JML \TYPE is the same as java.lang.Class the expression E1 <: E2 means the same thing as the expression E2.isAssignableFrom(E1).

• \type, which can be used to mark types in expressions. An expression of the form \type(T) has the type \TYPE. Since in JML \TYPE is the same as java.lang.Class, an expression of the form \type(T) means the same thing as T.class. For example, in

  \typeof(myObj) <: \type(PlusAccount)

  the use of \type(PlusAccount) is used to introduce the type PlusAccount into this expression context.

To avoid referring to the value of uninitialized locations, a constructor's precondition can only refer to locations in the object being constructed that are not assignable. This allows a constructor to refer to instance fields of the object being constructed if they are not made assignable by the constructor's assignable clause, for example, if they are declared with initializers. In particular, the precondition of a constructor may not mention a "blank final" instance variable that it must assign.

Since we are using Java expressions for predicates, there are some additional problems in mathematical modeling. We are excluding the possibility of side-effects by limiting the syntax of predicates, and by using type checking [Gifford-Lucassen86] [Lucassen87] [Lucassen-Gifford88] [Nielson-Nielson-Amtoft97] [Talpin-Jouvelot94] [Wright92] to make sure that only pure methods and constructors may be called in predicates.

Exceptions in expressions are particularly important, since they may arise in type casts. JML deals with exceptions by having the evaluation of predicates substitute an arbitrary expressible value of the normal result type when an exception is thrown during evaluation. When the expression's result type is a reference type, an implementation would have to return null if an exception is thrown while executing such a predicate. This corresponds to a mathematical model in which partial functions are mathematically modeled by underspecified total functions [Gries-Schneider95]. However, tools sometimes only approximate this semantics. In tools, instead of fully catching exceptions for all subexpressions, many tools only catch exceptions for the smallest boolean-valued subexpression that may throw an exception (and for entire expressions used in JML's measured-clause and variant-function).

JML will check that errors (i.e., exceptions that inherit from Error) are not explicitly thrown by pure methods. This means that they can be ignored during mathematical modeling. When executing predicates, errors will cause run-time errors.

3.2 Extensions to Java Expressions for Store-Refs

The grammatical production store-ref (see the JML Reference Manual [Leavens-etal-JMLRef] for the exact syntax) is used to name locations in the assignable and represents clauses. A store-ref names a location, not an object; a location is either a field of an object, or an array element. Besides the Java syntax of names and field and array references, JML supports the following syntax for store-refs. See the JML Reference Manual [Leavens-etal-JMLRef] for more details on the syntax.

• Array ranges, of the form A[E1 .. E2], denote the locations in the array A between the value of E1 and the value of E2 (inclusive). For example, the clause

  assignable myArray[3 .. 5]

  can be thought of an abbreviation for the following.

  assignable myArray[3], myArray[4], myArray[5]

• One can also name all the indexes in an array A by writing, A[*], which is shorthand for A[0 .. A.length-1].

• Two notations allow one to refer to the fields in some particular object.
  • The syntax x.* names all of the non-static fields of the object referred to by x. For example, if p is a Point object with two fields, x and y of type BigInteger, then p.* names the fields p.x and p.y. Notice that the fields of the BigInteger objects are not named. Also, p.*.* is not allowed.

  • If a is an array of type Rocket [], then the store-ref a[*].* means all of the non-static fields of each Rocket object referred to by the elements of array a.