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


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

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:

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 the JML Reference Manual [Leavens-etal-JMLRef] for syntactic details such as precedence):

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:

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 the JML Reference Manual [Leavens-etal-JMLRef] for the exact syntax) is used to name locations in the assignable, in, maps-into, and 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 the JML Reference Manual [Leavens-etal-JMLRef] for more details on the syntax.


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