[ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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
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:
=
),
and the various assignment operators (such as +=
, -=
, etc.)
++
and --
),
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):
(* 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) |
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.
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.
[
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] |
[*]
, which is shorthand for
A[0 ..
A.length-1]
.
.*
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.
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
.
[ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |