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, accessible, depends, represents clauses.

• Extensions to Java Expressions for Predicates
• 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 specification 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.(28)

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.

Also, expressions with side effects are permitted as arguments to the \duration and \working_space expressions, because their argument expressions are not evaluated.

JML adds the following new syntax to the Java expression syntax, for use in predicates (see section B.1.10 Predicate and Specification Expression Syntax 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 either side 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 section B.1.10 Predicate and Specification Expression Syntax) 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.
• \duration, which describes the specified maximum number of virtual machine cycle times needed to execute the method call or explicit constructor invocation expression that is its argument; e.g., \duration(myStack.push(o)) is the maximum number of virtual machine cycles needed to execute the call myStack.push(o), according to the contract of the static type of myStack's type's push method, when passed argument o. Note that the expression used as an argument to \duration should be thought of as quoted, in the sense that it is not to be executed; thus the method or constructor called need not be free of side effects. The argument expression must be a method call or explicit constructor invocation expression; the type of a \duration expression is long. For a given Java Virtual Machine, a virtual machine cycle is defined to be the minimum of the maximum over all Java Virtual Machine instructions, i, of the length of time needed to execute instruction i. The keyword \duration can only be used in the spec-expression of a duration-clause; it cannot be used, for example, in postconditions.
• \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.
• \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.(29)
• \invariant_for, which is true just when its argument satisfies the invariant of its static type; for example, \invariant_for((MyClass)o) is true when o satisfies the invariant of MyClass. The entire \invariant_for expression is of type boolean.
• \is_initialized, which is true just when its reference-type argument is a class that has finished its static initialization. It is of type boolean.
• \lblneg and \lblpos can be used to attach labels to expressions [Leino-Nelson-Saxe00]; these labels might be printed in various messages by support tools, for example, to identify an assertion that failed. Such an expression has a label and a body; for example, in

     (\lblneg indexInBounds 0 <= index && index < length)
  

  the label is indexInBounds and the body is the expression 0 <= index && index < length. The value of a labeled expression is the value of its body, hence its type is the type of its body. The idea is that if this expression is used in an assertion and its value is false (e.g., when doing run-time checking of assertions), then a warning will be printed that includes the label indexInBounds. The form using \lblpos has a similar syntax, but should be used for warnings when the value of the enclosed expression is true.
• \lockset, which is the set of locks held by the current thread. It is of type JMLObjectSet. (This is an adaptation from ESC/Java [Leino-etal00] [Leino-Nelson-Saxe00] for dealing with threads.)
• \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)
  

• \not_modified, which asserts that the values of objects (and their dependees) are the same in the post-state as in the pre-state; for example, \not_modified(xval,yval) says that xval and yval have the same value in the pre- and post-states (in the sense of an equals method). The keyword \not_modified can only be used in an ensures-clause or a signals-clause; it cannot be used, for example, in preconditions. The type of a \not_modified expression is boolean.
• \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.
• Several notations using \reach allow one to refer to the set of objects reachable from some particular object. The \reach syntax is overloaded to reduce the number of keywords. There are three cases, each of which has two alternatives depending on the static type of the first argument:
  • The syntax \reach(x) denotes the smallest JMLObjectSet containing the object denoted by x, if any, and all objects accessible through all fields of objects in this set. That is, if x is null, then this set is empty otherwise it contains x, all objects accessible through all fields of x, all objects accessible through all fields of these objects, and so on, recursively. If the expression x has static type org.jmlspecs.models.JMLObjectSet, then \reach(x) denotes the smallest JMLObjectSet containing the non-null objects in x, if any, and all objects accessible through all fields of objects in this set.
  • The syntax \reach(x, T) denotes the smallest JMLObjectSet containing the object denoted by x, if such an object exists and has type T, and all objects of type T accessible through all fields of objects in this set. If x, the argument to \reach has the static type org.jmlspecs.models.JMLObjectSet, then this syntax denotes the smallest JMLObjectSet containing the non-null objects in x of type T, if any, and all objects accessible through all fields of objects in this set. Note that if x is a JMLObjectSet, it may contain objects of different types; the presence of objects of other types does not matter. Only the instances of type T participate, and there need not be any instances of type T in the set.
  • The syntax \reach(x, T, f) denotes the smallest JMLObjectSet containing the object denoted by x, if such an object exists and has type T, and all objects of type T accessible using the field f on objects in this set. The type T must have been declared with a (non-static) field f. If x has static type org.jmlspecs.models.JMLObjectSet, then this denotes the smallest JMLObjectSet containing the objects in x that have type T, and all objects of type T accessible using the field f on objects in this set. More generally, in this syntax one can use instead of f, a store-ref-expression. For example, in

      \reach(myPointSet, ColorPoint, neighbor[3])
    

    if myPointSet is a JMLObjectSet, then this expression denotes the smallest set of objects of type ColorPoint such that the objects contained in myPointSet of type ColorPoint are in the set, and for each object cp of type ColorPoint in the set, cp.neighbor[3] is in the set.
• \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.
• \space, which describes the amount of heap space, in bytes, allocated to the object refered to by its argument; e.g., \space(myStack) is number of bytes in the heap used by myStack, not including the objects it contains. The type of the spec-expression that is the argument must be a reference type, and the result type of a \space expression is long. The keyword \space can only be used in the spec-expression of a working-space-clause; it cannot be used, for example, in postconditions.
• \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.
• \working_space, which describes the maximum specified amount of heap space, in bytes, used by the method call or explicit constructor invocation expression that is its argument; e.g., \working_space(myStack.push(o)) is the maximum number of bytes needed on the heap to execute the call myStack.push(o), according to the contract of the static type of myStack's type's push method, when passed argument o. Note that the expression used as an argument to \working_space should be thought of as quoted, in the sense that it is not to be executed; thus the method or constructor called need not be free of side effects. The argument expression must be a method call or explicit constructor invocation expression; the result type of a \working_space expression is long. The keyword \working_space can only be used in the spec-expression of a working-space-clause; it cannot be used, for example, in postconditions.

As in Java itself, most types are reference types, and hence many expressions yield references (i.e., object identities or addresses), as opposed to primitive values. This means that ==, except when used to compare pure values of primitive types such as boolean or int, is reference equality. As in Java, to get value equality for reference types one uses the equals method in assertions. For example, the predicate myString == yourString, is only true if the objects denoted by myString and yourString are the same object (i.e., if the names are aliases); to compare their values one must write myString.equals(yourString).

The reference semantics makes interpreting predicates that involve the use of \old interesting. We want to have the semantics suited for two purposes:

• execution of assertions for purposes of debugging and testing, as in Eiffel, and
• generation of mathematical assertions for static analysis and possible theorem proving (e.g., to verify program correctness).

The key to the semantics of \old is to treat it as an abbreviation for a local definition. That is, E in \old(E) can be evaluated in the pre-state, and its value bound to a locally defined name, and then the name can be used in the postcondition.

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 section B.1.5 Store Ref Syntax) is used to name locations in the assignable, depends, represents clauses. A similar production for object-ref is used in the accessible clause. 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 section B.1.4 Behavioral Specification Syntax for Types, 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].
• Several notations using \fields_of allow one to refer to the fields and array elements in a set of objects, or in some particular object. The \fields_of syntax is overloaded to reduce the number of keywords. There are three cases, each of which has two alternatives depending on the static type of the first argument:
  • The syntax \fields_of(x) names all of the non-static fields and array elements of the object(s) referred to by x. If the static type of x is org.jmlspecs.models.JMLObjectSet, then this names all the fields and array elements in all the objects in the set x, otherwise it simply names all the fields and array elements of the object x. For example, if p is a Point object with two fields, x and y of type BigInteger, then \fields_of(p) names the fields p.x and p.y. Notice that the fields of the BigInteger objects are not named. As another example, if a is an array of type Rocket [], then the store-ref \fields_of(a) is equivalent to a[*].
  • The syntax \fields_of(x, T) names all of the non-static fields and array elements of x, found in objects of type T. That is, either x must have type T (or a subtype), or if static type of x is org.jmlspecs.models.JMLObjectSet, then this names all non-static fields of all instances of type T (or a subtype) in the set x, otherwise x must have static type T (or a subtype), this store-ref names all the non-static fields of x found in type T (or the array elements of x, if T is an array type.) Note that if x is a JMLObjectSet, it may contain objects of different types; the presence of objects of other types does not matter. Only the instances of type T participate, and there need not be any instances of type T in the set.
  • The syntax \fields_of(x, T, f) names the f fields of x in objects of type T. The type T must have been declared with a (non-static) field f. Note that in this case, T cannot be an array type. If x has static type org.jmlspecs.models.JMLObjectSet, then this names the f fields in all instances of type T in the set x, otherwise x must have static type T, this store-ref is the same as writing x.f. More generally, in this syntax one can use instead of f, a store-ref-expression. For example, in

      \fields_of(myPointSet, ColorPoint, val[3].color)
    

    if myPointSet is of type JMLObjectSet, then this expression refers to the locations cp.val[3].color, for each object cp of type ColorPoint in myPointSet.

Note that \reach is useful for constructing sets of objects for use as the first argument to \fields_of. For example, one might write \fields_of(\reach(myVar)).

Go to the first, previous, next, last section, table of contents.