[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

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:

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):

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.


[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

This document was generated by Gary Leavens on March, 16 2009 using texi2html