[ << ] | [ >> ] | [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.
11.1 Predicates 11.2 Specification Expressions 11.3 Expressions 11.4 JML Primary Expressions 11.5 Set Comprehensions 11.6 JML Operators 11.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 11.2 Specification Expressions, for the syntax of specification expressions.
predicate ::= spec-expression |
The following gives the syntax of specification expressions in JML. See section 11.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 11.4 JML Primary Expressions) and
set-comprehension (see section 11.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 11.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 12. 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
reached the statement the label is attached to.
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.
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.
It is a type error if \old()
or \pre()
encloses a free occurrence of a
quantified variable. For example, in the following,
\old()
encloses a free occurrence of the quantified variable
i
, which is declared in the surrounding quantifier, and thus
the example is illegal.
(\forall int i; 0 <= i && i < 7; \old(i < y)) // illegal |
\old(i < y)
in the pre-state.
However, constructions like the following are legal, as in the first
the use of \old()
does not enclose the quantified variable,
i
, and in the second use of \old()
does not enclose a
free occurrence of the quantified variable (the variable is bound by
the declaration which is inside of \old()
.
(\forall int i; 0 <= i && i < 7; i < \old(y)) // ok \old((\forall int i; 0 <= i && i < 7; i < y)) // ok |
\not_assigned
The syntax of a not-assigned-expression is as follows. See section 11.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 11.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 11.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 11.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 11.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 11.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 11.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 11.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 11.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 11.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 11.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 11.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 11.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 11.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 11.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 11.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 11.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 E.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.
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 result in identical sets:
new JMLObjectSet {Integer i | s.has(i) && 0 < i.intValue() } new JMLObjectSet {Object i | s.has(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.
11.6.1 Subtype operator 11.6.2 Equivalence and Inequivalence Operators 11.6.3 Forward and Reverse Implication Operators 11.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.
JML extends these two operators, but not
>
and >=
, as comparisons on Objects.
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.
store-ref-list ::= store-ref-keyword | store-ref [ |
A store-ref denotes a set of locations in general.
The form \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 the tool.
The form SR.*
refers to all fields of the object denoted by SR.
Similarly, the form A[*]
refers to all locations of
elements in the array A. [[[ And their datagroups? - DRC]]]
Otherwise if a store-ref refers to a field, it denotes that field's data group (see section 10. Data Groups). If a store-ref refers to an element or a range of elements, it refers to all of the named locations in that array.
[ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |