| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This chapter describes predicates in JML and JML's extensions to Java's expressions. It also describes store references, which are similar to specification expressions, but are used to describe locations instead of values. Details are found in the sections below.
12.1 Predicates 12.2 Specification Expressions 12.3 Expressions 12.4 JML Primary Expressions 12.5 Set Comprehensions 12.6 JML Operators 12.7 Store Refs
A predicate The following gives the syntax of predicates, which are simply spec-expressions that must have a boolean value. See section 12.2 Specification Expressions, for the syntax of specification expressions.
predicate ::= spec-expression |
The following gives the syntax of specification expressions in JML. See section 12.3 Expressions, for the syntax of expression.
spec-expression-list ::= spec-expression
[ |
Within a spec-expression, one cannot use any of the operators
(such as ++, --, and the assignment operators) that
would necessarily cause side effects. In addition, one can use
extensions that are specific to JML, in particular the JML primary
expressions.
The JML syntax for expressions extends the Java syntax with several operators and primitives.
The precedence of operators in JML expressions is similar to that in Java
The precedence levels are given in the following table,
where the parentheses, quantified expressions,
[], ., and method calls
on the first three lines all have the highest precedence,
and for the rest, only the operators on the same line have the same precedence.
highest |
The following is the syntax of Java expressions, with JML additions.
The additions are
the operators ==>, <==, <==>, <=!=>,
and <:, and the syntax found under the
nonterminals jml-primary
(see section 12.4 JML Primary Expressions) and
set-comprehension (see section 12.5 Set Comprehensions).
The JML additions to the Java syntax can only be used
in assertions and other annotations.
Furthermore, within assertions, one cannot use any of the operators
(such as ++, --, and the assignment operators) that
would necessarily cause side effects.
expression-list ::= expression [ |
[[[Need to have semantics of the new things explained here.]]]
The following is the syntax of jml-primary.
jml-primary ::= result-expression
| old-expression
| not-assigned-expression
| not-modified-expression
| only-accessed-expression
| only-assigned-expression
| only-called-expression
| only-captured-expression
| fresh-expression
| reach-expression
| duration-expression
| space-expression
| working-space-expression
| nonnullelements-expression
| informal-description
| typeof-expression
| elemtype-expression
| type-expression
| lockset-expression
| max-expression
| is-initialized-expression
| invariant-for-expression
| lblneg-expression
| lblpos-expression
| spec-quantified-expr
|
All of the JML keywords that can be used in expressions which would
otherwise start with an alphabetic character
start with a backslash (\),
so that they cannot clash with the program's variable names.
The new expressions that JML introduces are described below. Several of the descriptions below quote, without attribution, descriptions from [Leavens-Baker-Ruby06].
\result The syntax of a result-expression is as follows.
result-expression ::= |
The primary \result can only be used in ensures,
duration, and workingspace
clauses of a non-void method. Its value is the value returned by the
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.
\old and \pre An old-expression has the following syntax. See section 12.2 Specification Expressions, for the syntax of spec-expression.
old-expression ::= |
An expression of the form
\old(Expr) refers to the value that the expression
Expr had in the pre-state of a method.
JML uses Java's reference semantics, hence the pre-state value of an
expression whose type is a reference type is simply the reference;
it is not a clone of the object the reference points to.
For example, suppose in the pre-state that
v is field that holds a reference to a HashMap;
concretely, suppose that the location stored in v is
0x952ab340. Then the expression \old(v) denotes the pre-state value
of v, which is the same reference, i.e.,
it is the address 0x952ab340. Note that \old(v) is not a
reference to a copy of the HashMap stored at that location, but
simply a copy of the location's address (the reference), which is the
value of v. If the fields of the object
at that location have changed in the post-state, then changes to those
fields will be visible through \old(v); for example,
\old(v).size() will be the same as v.size().
To write a post-condition that refers to v's size in the pre-state,
one should instead write \old(v.size()).
Indeed as a general rule, it is always safest to use \old() only around
expressions whose type is a value type or a type with immutable
values, such as String.
Expressions of this form may be used in both normal and exceptional
postconditions (see section 9. Method Specifications,
for more about such ensures and signals clauses),
in history constraints, in duration and working space clauses,
and also in assertions that appear in the bodies of methods
(see section 13. Statements and Annotation Statements, for more about
assert and assume statements, loop
invariants, and variant functions).
However, we recommend that inside the bodies of methods, one of the
two other forms of old-expression (see below) be used instead.
The reason for this is that the reader
may wonder whether \old(Expr) in the body of a method means
the pre-state value of Expr (which it does) or the value of
Expr before some previous statement (which it does not).
An expression of the form
\pre(Expr) also refers to the value that the expression
Expr had in the pre-state of a method.
Expressions of this form may only be used in assertions that appear in
the bodies of methods
(i.e., in assert and assume statements, and in loop
invariants and variant functions).
That is, such expressions may not be used in specification cases, and
hence may not appear in normal or exceptional
postconditions, in history constraints, or in duration and working
space clauses.
An expression of the form
\old(Expr, Label)
refers to the value that the expression
Expr had when control last reached the statement label Label.
That is, it refers to the value of the expression just before control
last reached the statement the label is attached to.
Expressions of this form may only be used when the Label has been
declared in a surrounding context.
Thus such expressions may be used in assert and assume
statements, and in loop invariants and variant functions, where such a
label has been declared.
They may also be used in specification cases that occur in model program
spec-statement (see section 15.6 Specification Statements)
and in the refining-statements (see section 13.4.3 Refining Statements).
In an expression of the form
\old(Expr, Label),
Label must be a label defined in the current method.
The type of
\old(Expr),
\old(Expr, Label),
or \pre(Expr),
is simply the type of Expr.
\not_assigned The syntax of a not-assigned-expression is as follows. See section 12.7 Store Refs, for the syntax of store-ref-list.
not-assigned-expression ::= |
The JML operator \not_assigned can be used in both normal and
exceptional preconditions (i.e., in ensures and signals
clauses), and in history constraints. It asserts that the locations
in the data group (see section 10. Data Groups) named by the argument were not
assigned to during
the execution of the method being specified (or all methods to which a
history constraint applies).
For example, \not_assigned(xval,yval) says that the locations
in the data groups named by xval and yval were not
assigned during the method's execution.
A predicate such as \not_assigned(x.f) refers to the entire
data group named by x.f not just to the location x.f
itself. This allows one to specify absence of even temporary
side-effects in various cases of a method.
See section 12.4.4 \not_modified, for ways to specify that just the value
of a given field was not changed, which allows temporary side effects.
The \not_assigned operator can be applied to both concrete and
model or ghost fields. When applied to a model field, the meaning is
that all (concrete) locations in that model field's data group were
not assigned.
[[[A real example would help here.]]]
The type of a \not_assigned expression is boolean.
\not_modified The syntax of a not-modified-expression is as follows. See section 12.7 Store Refs, for the syntax of store-ref-list.
not-modified-expression ::= |
The JML operator \not_modified can be used in both normal and
exceptional preconditions (i.e., in ensures and signals
clauses), and in history constraints. It asserts that the values of
the named fields are the same in the post-state as in the pre-state;
for example, \not_modified(xval,yval) says that the fields
xval and yval
have the same value in the pre- and post-states
(in the sense of the equals method for their types).
A predicate such as \not_modified(x.f) refers to the location
named by x.f, not to the entire data group of x.f. This
allows one to specify benevolent side-effects, as one can name
x.f (or a data group in which it participates) in an assignable
clause, but use \not_modified(x.f) in the postcondition.
See section 12.4.3 \not_assigned, for ways to specify that no assignments
were made to any location in a data group, disallowing temporary side effects.
The \not_modified operator can be applied to both concrete and
model or ghost fields. When applied to a model field, the meaning is
that only the value of the model field is unchanged (in the sense of
its type's equals operation); concrete fields involved in its
representation may have changed.
[[[A real example would help here.]]]
The type of a \not_modified expression is boolean.
\only_accessed The syntax of an only-accessed-expression is as follows. See section 12.7 Store Refs, for the syntax of store-ref-list.
only-accessed-expression ::= |
The JML operator \only_accessed can be used in both normal and
exceptional preconditions (i.e., in ensures and signals
clauses), and in history constraints. Used in a method's
postcondition (perhaps implicitly in a history constraint), it asserts
that the method's execution only reads from a subset of the data groups
named by the given fields.
For example, \only_accessed(xval,yval) says that no fields,
outside of the data groups of xval and yval were read by
the method. This includes both direct reads in the body of the
method, and reads during calls that were made by the method (and
methods those methods called, etc.).
A predicate such as \only_accessed(x.f) refers to the entire
data group named by x.f not just to the location x.f
itself.
The \only_accessed operator can be applied to both concrete and
model or ghost fields. When applied to a model field, the meaning is
that the (concrete) locations in that model field's data group are
permitted to be accessed during the method's execution.
The type of an \only_accessed expression is boolean.
\only_assigned The syntax of an only-assigned-expression is as follows. See section 12.7 Store Refs, for the syntax of store-ref-list.
only-assigned-expression ::= |
The JML operator \only_assigned can be used in both normal and
exceptional preconditions (i.e., in ensures and signals
clauses), and in history constraints. Used in a method's
postcondition (perhaps implicitly in a history constraint), it asserts
that the method's execution only assigned to a subset of the data groups
named by the given fields.
For example, \only_assigned(xval,yval) says that no fields,
outside of the data groups of xval and yval were assigned by
the method. This includes both direct assignments in the body of the
method, and assignments during calls that were made by the method (and
methods those methods called, etc.).
A predicate such as \only_assigned(x.f) refers to the entire
data group named by x.f not just to the location x.f
itself.
The \only_assigned operator can be applied to both concrete and
model or ghost fields. When applied to a model field, the meaning is
that the (concrete) locations in that model field's data group are
permitted to be assigned during the method's execution.
The type of an \only_assigned expression is boolean.
\only_called The syntax of an only-called-expression is as follows. See section 8.3 Constraints, for the syntax of method-name-list.
only-called-expression ::= |
The JML operator \only_called can be used in both normal and
exceptional preconditions (i.e., in ensures and signals
clauses), and in history constraints. Used in a method's
postcondition (perhaps implicitly in a history constraint), it asserts
that the method's execution only called from a subset of methods given
in the method-name-list.
For example, \only_called(p,q) says that methods, apart from
p and q, were called during this method's execution.
The type of an \only_called expression is boolean.
\only_captured The syntax of an only-captured-expression is as follows. See section 12.7 Store Refs, for the syntax of store-ref-list.
only-captured-expression ::= |
The JML operator \only_captured can be used in both normal and
exceptional preconditions (i.e., in ensures and signals
clauses), and in history constraints. Used in a method's
postcondition (perhaps implicitly in a history constraint), it asserts
that the method's execution only captured references from a subset of
the data groups named by the given fields.
For example, \only_captured(xv,yv) says that no references,
outside of the data groups of xv and yv were captured by
the method.
A reference is captured when it is stored into a field (as
opposed to a local variable). Typically a method captures a formal
parameter (or a reference stored in a static field) by assigning it to
a field in the method's receiver (the this object), a field in
some object (or to an array element), or to a static field.
A predicate such as \only_captured(x.f) refers to the
references stored in the entire data group named by x.f in the
pre-state, not just to those stored in the location x.f itself.
However, since the references being captured are usually found in
formal parameters, the complications of data groups can usually be ignored.
The \only_captured operator can be applied to both concrete and
model or ghost fields. When applied to a model field, the meaning is
that the (concrete) locations in that model field's data group are
permitted to be captured during the method's execution.
The type of an \only_captured expression is boolean.
\fresh The syntax of a fresh-expression is as follows. See section 12.2 Specification Expressions, for the syntax of spec-expression-list.
fresh-expression ::= |
The operator \fresh 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.
Note that it is wrong to use \fresh(this) in the specification
of a constructor, because Java's new operator allocates storage
for the object; the constructor's job is just to initialize that
storage.
\reach The syntax of a reach-expression is as follows. See section 12.2 Specification Expressions, for the syntax of spec-expression.
reach-expression ::= |
The \reach expression
allows one to refer to the set of objects reachable from some particular object.
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 x denotes a model field (or data group), then
\reach(x)
denotes the smallest JMLObjectSet containing the objects
reachable from x or reachable from the objects referenced by
fields in that data group.
\duration The syntax of a duration-expression is as follows. See section 12.3 Expressions, for the syntax of expression.
duration-expression ::= |
\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.
Note that the argument to \duration is an
expression instead of just the name of a method,
because different method calls, i.e., those with different parameters,
can take different amounts of time [Krone-Ogden-Sitaraman03].
The argument expression passed to \duration
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.
\space The syntax of a space-expression is as follows. See section 12.2 Specification Expressions, for the syntax of spec-expression. [[[ Shouldn't this take an expression instead of a spec-expression? - DRC]]]
space-expression ::= |
\space, which describes the amount of heap space, in bytes,
allocated to the object referred to by its argument [Krone-Ogden-Sitaraman03];
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.
\working_space working-space-expression ::= |
\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 detailed arguments are needed in the specification of the call
because different method calls, i.e., those with different parameters,
can use take different amounts of space [Krone-Ogden-Sitaraman03].
The argument expression must be a method call or explicit constructor
invocation expression; the result type of a \working_space
expression is long.
\nonnullelements The syntax of a nonnullelements-expression is as follows. See section 12.2 Specification Expressions, for the syntax of spec-expression.
nonnullelements-expression ::= |
The operator \nonnullelements
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)
|
An informal-description is some text enclosed in (* and
*).
See section 4.6 Tokens, for details of its syntax.
It is used as an escape form formality.
An informal description used as a predicate has type boolean.
Hence the text in an informal description should describe a condition,
for example (* the value of x is displayed *).
The value of an informal description is only known to the user, not to any JML tools, so it is never executable. Informal descriptions should thus be avoided when possible, but can be used to avoid formalizing everything when doing so would be too expensive.
\typeof The syntax of a typeof-expression is as follows. See section 12.2 Specification Expressions, for the syntax of spec-expression.
typeof-expression ::= |
The operator \typeof 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.
\elemtype The syntax of a elemtype-expression is as follows.
elemtype-expression ::= |
The \elemtype operator 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 (see section 7.1.2.2 Type-Specs). If the argument is not an array type,
then the result is null. For example, \elemtype(\type(int))
and \elemtype(\type(Object)) are both null.
\type The syntax of a type-expression is as follows. See section 7.1.2.2 Type-Specs, for the syntax of type.
type-expression ::= |
\type can be used to introduce literals of type
\TYPE in expressions.
An expression of the form \type(T),
where T is a type name, 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, if T is a reference type.
If T is a primitive type, then \type(T) is equivalent to the value
of the TYPE field of the corresponding reference type. Thus
\type(boolean) equals Boolean.TYPE.
For example, in
\typeof(myObj) <: \type(PlusAccount) |
the use of \type(PlusAccount) is used to introduce
the type PlusAccount into this expression context.
\lockset The syntax of a lockset-expression is as follows.
lockset-expression ::= |
The \lockset primitive denotes
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.)
\max The syntax of a max-expression is as follows. See section 12.2 Specification Expressions, for the syntax of spec-expression.
max-expression ::= |
\max operator returns the "largest" (as defined by <) of a
set of lock objects, given a lock set as an argument. The result is of type Object.
(This is an adaptation from ESC/Java [Leino-etal00]
[Leino-Nelson-Saxe00] for dealing with threads.)
If you are looking to take the maximum of several integers, use the max quantifier (see section 12.4.24.2 Generalized Quantifiers).
\is_initialized The syntax of the is-initialized-expression is as follows. See section 7.1.2.2 Type-Specs, for the syntax of reference-type
is-initialized-expression ::= |
The \is_initialized operator returns true just when its
reference-type argument is a class that has finished its static
initialization. It is of type boolean.
\invariant_for invariant-for-expression ::= |
The \invariant_for operator returns 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.
\lblneg and \lblpos The syntax of the two kinds of labeled expressions is as follows. See section 12.2 Specification Expressions, for the syntax of spec-expression.
lblneg-expression ::= |
Parenthesized expressions that start with
\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.
spec-quantified-expr ::= |
Note that each quantified expression includes a set of parentheses; these
parentheses cannot be omitted. The first part of a quantified expression is
the quantifier, which determines the operation to be performed. Every
quantifier starts with a backslash (\). Following the quantifier are
quantified-var-decls, which declare bound variables whose scope is
the spec-quantified-expr. The bound variables may not conflict with
existing local variables, but may hide static and instance fields. The
optional predicate between the two semicolons is the range predicate; a
quantifier ranges over all possible values of its bound variables that satisfy
the range predicate (for a discussion of the ranges of values for reference
types, see section 12.4.24.6 Quantifying over Reference Types). If the range predicate is
omitted, it defaults to true. The final spec-expression is called
the body of the quantifier.
We discuss the various kinds of quantified expressions below.
The quantifiers
\forall and \exists,
are universal and existential quantifiers (respectively).
For example,
(\forall int i,j; 0 <= i && i < j && j < 10; a[i] < a[j]) |
says that the values a[0] ... a[9] are sorted.
The body of a universal or existential quantifier must be of type
boolean. The type of a universal or existential quantified expression
as a whole is boolean. When the range predicate is not satisfiable, the value of a \forall expression is true and the value of an \exists expression is false. For example:
(\forall int i; 0 < i && i < 0; 0 < i) == true (\exists int i; 0 < i && i < 0; 0 < i) == false |
The quantifiers \max, \min, \product, and
\sum, 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 expression in the body must be of 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. 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. [[[ This would depend on the arithmetic mode in force - DRC]]]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. [[[ Or should this be undefined - DRC]]]
The numerical quantifier, \num_of, returns the number of values
for its variables for which the range and the expression in its body
are true. 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) |
When are universal or existential quantifiers executable for purposes
of runtime assertion checking?
If the type of the quantified variable is boolean, then it is
always executable. Otherwise a spec-quantified-expr
is only executable if the form of the expression
matches a pattern that the runtime assertion checker understands.
This varies by tool implementation, but you can expect that the
runtime assertion checker understands patterns where the range predicate
gives a finite range for an ordinal primitive value type (such as
int) or where the range predicate requires the quantified
variable to be drawn from some set.
Examples include the following.
[[[Make these examples be real examples in the samples directory]]]
(\forall int x; 0 <= x && x < somelimit; ...)
(\forall Object x; someSet.has(x); ...)
|
You should get warnings from the jmlc tool
when assertions are not executable,
but you have to use the -w2 flag to see them.
If a spec-quantified-expr, QE, is executable, then a tool executing it should only evaluate any range expression in QE once per execution of QE. Since the value of such a range expression cannot change, this evaluation strategy will not change the value of QE, but it will save time to only evaluate the range expression once for each evaluation of QE.
bound-var-modifiers ::= |
Logical variables can be bound in
Note that in JML, non_null and nullable are not reserved
words, hence such identifiers can be used as type names. In order to
quantify over the elements of a type named non_null or
nullable is necessary to provide an explicit nullity
modifier. For example,
(\forall non_null non_null nn; ...) |
non_null is one of the bound-var-modifiers and
the second is the type non_null.
The range of values for a quantified variable that is declared to be of a reference type:
null unless the bound variable is declared
nullable (see section G.2.1 Non-null by Default).
The syntax of a set-comprehension expression is as follows.
set-comprehension ::= |
The set comprehension notation can be used to succinctly define sets.
The meaning of a new-expr (see section 12.3 Expressions)
with a set-comprehension suffix,
such as
new ST { T x | s.has(x)
&& P(x) }
is to form a subset, of type ST, of the set s,
which contains just those elements x that are both in s and
for which P(x) is true.
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.intValue() && i.intValue() <= 10 }
|
The syntax of JML limits set comprehensions so that the postfix-expr
following the vertical bar (|) is always a method invocation with the
bound variable declared in the quantified-var-declarator as its
parameter; the method may be either the has method of an
org.jmlspecs.models.JMLObjectSet or
org.jmlspecs.models.JMLValueSet, or the contains method of a
java.util.Collection. This restriction is used to avoid Russell's
paradox [Whitehead-Russell25]. The bound variable, whose scope is the
set-comprehension, may not conflict with existing local variables, but
may hide static and instance fields. The bound variable type is used to
restrict the objects that become part of the resulting set; if the set
called in the postfix-expr contains objects that are not
assignable to the bound variable, they are not contained in the
resulting set comprehension. Thus, the following two set comprehension
expressions (given an existing Collection s) result in identical sets:
new JMLObjectSet {Integer i | s.contains(i) && 0 < i.intValue() }
new JMLObjectSet {Object i | s.contains(i) && i instanceof Integer &&
0 < ((Integer) i).intValue() }
|
In practice, one starts either from some relevant set at hand or from the sets
found in JMLObjectSet and JMLValueSet containing the objects of
primitive types. The type of a set comprehension is the type named following
new, which must be JMLObjectSet or JMLValueSet. The bound
variable type must be compatible with the set comprehension type; in
particular, the bound variable type must be a subtype of
org.jmlspecs.models.JMLType if the set comprehension type is
JMLValueSet.
In this section we describe the various new operators that JML adds to Java expressions. The following can all be used in spec-expressions.
12.6.1 Subtype operator 12.6.2 Equivalence and Inequivalence Operators 12.6.3 Forward and Reverse Implication Operators 12.6.4 Lockset Ordering
The relational operator <: 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).
As a result, primitive types are not subtypes of java.lang.Object,
nor of each other, though they are of themselves; so, for example, Integer.TYPE <: Integer.TYPE is true.
The operators <==> and <=!=> work only on
boolean-subexpressions and have the same meaning as == and
!=, respectively. However, they have very low precedence, and
so are useful at the top-level of a spec-expression.
Unlike == and !=, the
operators <==> and <=!=> are also associative and symmetric.
The notation <==> can be read "if and only if". It has the same
meaning for Boolean values as ==, but has a lower precedence.
Therefore, the expression "\result <==> size == 0"
means the same thing as "\result == (size == 0)".
The notation <=!=> can be read "is not equivalent to".
It has the same meaning for Boolean values as !=, but has a
lower precedence. Therefore, the expression "\result <=!=> size == 0"
means the same thing as "\result != (size == 0)".
The expressions on either side of these operators must be of type
boolean, and the type of the result is also boolean.
The operators ==> and <== work only on
boolean-subexpressions. They compute forward and reverse
implications, respectively.
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.
These two operators are evaluated in short-circuit fashion, left to right.
Thus, in a ==> b, if a is false, then the expression is true
and b is not evaluated. Similarly, in a <== b, if a is true, the expression is true and b is not evaluated. In other words, a ==> b is equivalent to !a || b and a <== b is equivalent to a || !b.
Because of this short-circuit evaluation, a ==> b is not quite
equivalent to b <== a. For example, x != null ==> x.a > 0
will be true if x is null, but x.a>0 <== x != null
would be undefined (or throw a NullPointerException) if x is null.
JML uses
<# and <#= to test order of locks.
(The previously-used operators < and <= were deprecated because their use conflicts with the Java comparisons defined for those operators when autoboxing is available.)
Using synchronized statements, Java
programs can establish monitor locks to permit only one thread at a
time to execute given sections of code. Any object can be used as
a lock. In order for ESC/Java [Leino-Nelson-Saxe00] to
reason about the possibility of deadlocks among threads, a partial order
must be statically declared on lock objects, with "larger" objects
being objects whose locks should be acquired later. ESC/Java suggests
the use of axiom-clauses to declare this partial order.
The <# and <#= operators test this partial order in assertions.
When used in this way, the subexpressions to either side of <#
or <#= must be reference types, and the result is of type boolean.
The syntax related to the store-ref production is used in several places, in particular in assignable clauses (see section 9.9.9 Assignable Clauses).
store-ref-list ::= store-ref-keyword | store-ref [ |
A store-ref denotes a set of locations. These sets can be specified using data groups (see section 10. Data Groups), and if this is done then the set of locations denoted by a store-ref is the union of all the sets of locations in the specified set of data groups.
The set of locations denoted by a store-ref-list of the form
store-ref, [ store-ref ] ... is the union
of all the sets of locations denoted by each store-ref in the list.
The store-ref \nothing denotes the empty set of locations.
The form \everything denotes the set of all locations in the program.
The form \not_specified denotes a unspecified set of locations,
whose usage is determined by a particular tool.
When SR denotes a set of locations contain objects,
then SR.f, where f is an ident,
denotes the union of the data groups of each
field named f in each object in the denotation of SR.
The meaning of a store-ref-expression of the form SR.*
depends on the denotation of the stor-ref-name SR.
When SR denotes a set of locations of objects,
then SR.* denotes the
union of the data groups of all visible
instance fields of SR's (static) type.
On the other hand, if SR names a class or interface, then
SR.* denotes the union of the data groups of all visible static
fields of the named class or interface.
Similarly, when SR denotes a set of locations containing arrays,
then SR[*] denotes the union of all data groups
of all elements in all the arrays denoted by SR.
Also, when SR denotes a set of locations containing arrays,
then SR[L..H]
denotes the union of all data groups of all
elements in the arrays denoted by SR whose indexes
are between L and H inclusive.
In the case where SR denotes a set of locations containing arrays,
then SR[J]
denotes the union of all data groups of those arrays at the index
denoted by the spec-expression J.
| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |