In this section we give some examples of JML class specifications that illustrate the basic features of JML.
A simple example of an abstract class specification is the ever-popular
UnboundedStack type,
which is presented below.
It would appear in a file named `UnboundedStack.java'.
package org.jmlspecs.samples.stacks;
//@ model import org.jmlspecs.models.*;
public abstract class UnboundedStack {
/*@ public model JMLObjectSequence theStack;
@ public initially theStack != null && theStack.isEmpty();
@*/
//@ public invariant theStack != null;
/*@ public normal_behavior
@ requires !theStack.isEmpty();
@ assignable theStack;
@ ensures theStack.equals(\old(theStack.trailer()));
@*/
public abstract void pop( );
/*@ public normal_behavior
@ assignable theStack;
@ ensures theStack.equals(\old(theStack.insertFront(x)));
@*/
public abstract void push(Object x);
/*@ public normal_behavior
@ requires !theStack.isEmpty();
@ assignable \nothing;
@ ensures \result == theStack.first();
@*/
public /*@ pure @*/ abstract Object top( );
}
The above specification contains the declaration of a model field, an invariant, and some method specifications. These are described below.
In the fourth non-blank line of `UnboundedStack.java',
a model data field, theStack,
is declared.
Since it is declared using the JML modifier model,
such a field does not have to be implemented;
however, for purposes of the specification we treat much like any other
Java field (i.e., as a variable location).
That is, we imagine that each instance of the class UnboundedStack
has such a field.
The type of the model field theStack
is a type designed for mathematical modeling,
JMLObjectSequence.
Objects of this type are sequences of objects.
This type is provided by JML in the package org.jmlspecs.models,
which is imported in the second non-blank line of the figure.
Note that this import declaration does not have to appear
in the implementation, since it is modified by the keyword model.
In general, any declaration form in Java can have this modifier,
with the same meaning. That is, a model declaration is only
used for specification purposes, and does not have to appear in
an implementation.
At the end of the model field's declaration
above
is an initially clause.
(Such clauses are adapted from RESOLVE [Ogden-etal94]
and the refinement calculus
[Back88] [Back-vonWright98] [Morgan-Vickers94] [Morgan94].)
Model fields cannot be explicitly initialized (and thus cannot be
final), because there is no storage directly associated with them.
However, one can use an initially clause to describe an
abstract initialization for a model field.
Initially clauses can be attached to any field declaration, including
non-model fields, and permit one to constrain the initial values
of such fields.
Knowing something about the initial value of the field
permits data type induction [Hoare72a] [Wing83]
for abstract classes and interfaces.
The initially clause must appear to be true
of the field's starting value.
That is,
all reachable objects of the type UnboundedStack
must appear to have been created
as empty stacks and subsequently modified using the type's methods.
Following the model field declaration is an invariant.
An invariant does not have to hold during the execution
of an object's methods,
but it must hold, for each reachable object
in each publicly visible state;
i.e., for each state outside of a public method or constructor's execution,
and at the beginning and end of each public method's
execution.(8)
The figure's invariant just says that the value of theStack
should never be null.
Following the invariant are the specifications of
the methods pop, push, and top.
We describe the new aspects of these specifications below.
The use of the assignable(9)
clauses in the behavioral
specifications of pop and push
is interesting (and another difference from Eiffel).
These clauses give frame conditions [Borgida-Mylopoulos-Reiter95].
In JML, the frame condition given by a method's assignable clause
only permits the method to assign to a location, loc, if:
assignable clause,
assignable clause (see section 2.2 Data Groups),
For example, push's specification says that it may only
assign to theStack (and locations in theStack's data group).
This allows push to assign to theStack
(and the members of its data group), or to call some other method that
makes such an assignment.
Furthermore, push may assign to the formal parameter
x itself, even though that location is not listed in the
assignable clause, since x is local to the method.
However, push may not assign to fields not mentioned in the
assignable clause; in particular it may not assign to fields
of its formal parameter
x,(10)
or call a method that makes such an assignment.
The design of JML is intended to allow tools to
statically check the body of a method's implementation
to determine whether its assignable clause is satisfied.
This would be done by checking each assignment statement
in the implementation to see if
what is being assigned to is a location
that some assignable clause permits.
It is an error to assign to any other allocated, non-local location.
However, to do this, a tool must conservatively track aliases
and changes to objects containing the locations in question.
Also, arrays can only be dynamically checked, in general.(11)
Furthermore, JML will flag as an error
a call to a method that would assign
to locations that are not permitted by the calling method's
assignable clause.
It can do this using the assignable clause of the called method.
In JML, a location is modified by a method when it
is allocated in both the pre-state of the method,
reachable in the post-state,
and has a value that is different in these two states.
The pre-state of a method call is the state
just after the method is called and parameters have been evaluated and passed,
but before execution of the method's body.
The post-state of a method call is the state
just before the method returns or throws an exception;
in JML we imagine that \result and information about exception results
is recorded in the post-state.
Since modification only involves objects allocated in the pre-state,
allocation of an object, using Java's new
operator, does not itself cause any modification.
Furthermore, since the fields of new objects are locations
that were not allocated when the method started execution,
they may be assigned to freely.
The reason assignments to local variables are permitted
by the assignable clause is that
a JML specification takes the client's (i.e., the caller's) point of view.
From the client's point of view, the local variables in a method
are newly-allocated, and thus assignments to such variables are invisible
to the client.
Hence, in JML, it is an error to list formal parameters,
or other local variables, in the assignable clause.
Furthermore, when formal parameters are used in a postcondition,
JML interprets these as meaning the value initially given to the formal
in the pre-state,
since assignments to the formals within the method
do not matter to the client.
JML's interpretation of the assignable clause does not permit either temporary side effects or benevolent side effects. A method with a temporary side effect assigns a location, does some work, and then assigns the original value back to that location. In JML, a method may not have temporary side effects on locations that it is not permitted to modify [Ruby-Leavens00]. A method has a benevolent side effect if it assigns to a location in a way that is not observable by clients. In JML, a method may not have benevolent side effects on locations that it is not permitted to modify [Leino95] [Leino95a].
Because JML's assignable clauses give permission
to assign to locations, it is safe for clients to assume that
only the listed locations (and locations of their data group members)
may have their values modified.
Because locations listed in the assignable clause are the only
ones that can be modified, we often speak of what locations a method can
"modify," instead of the more precise "can assign to."
What does the assignable clause say about the modification of locations? In particular, although the "location" for a model field or model variable cannot be directly assigned to in JML, its value is determined by the concrete fields and variables that it (ultimately) depends on, specifically the members of its data group. That is, a model field or variable can be modified by assignments to the concrete members of its data group (see section 2.2 Data Groups). Thus, a method's assignable clause only permits the method to modify a location if the location:
assignable clause,
assignable
clause (see section 2.2 Data Groups),
In the specification of top,
the assignable clause says that a call to top that satisfies
the precondition cannot assign to any locations.
It does this by using the store-ref "\nothing."
Unlike some formal specification languages (including Larch BISLs and
older versions of JML),
when the assignable clause is omitted in a heavyweight
specification, the default store-ref for the assignable
clause is \everything.
Thus an omitted assignable clause in JML means that the method can assign
to all locations (that could otherwise be assigned to by the method).
Such an assignable clause plays havoc with formal
reasoning, and thus if one cares about verification, one should give
an assignable clause explicitly if the method is not pure
(see section 2.3.1 Purity).
When a method can modify some locations, they may have different
values in the pre-state and post-state of a call.
Often the post-condition must refer to the values held
in both of these states.
JML uses a notation similar to Eiffel's to refer
to the pre-state value of a variable.
In JML the syntax is \old(E), where E is an expression.
(Unlike Eiffel, we use parentheses following \old
to delimit the expression to be evaluated in the pre-state explicitly.
JML also uses backslashes (\\) to mark the keywords it uses in
expressions; this avoids interfering with Java program identifiers,
such as "old".)
The meaning of \old(E) is as if E were evaluated
in the pre-state and that value is used in place of
\old(E) in the assertion.
It follows that, an expression like \old(myVar).theStack
may not mean what is desired,
since only the old value of myVar is saved;
access to the field theStack is done in the post-state.
If it is the field, theStack, not the variable, myVar,
that is changing, then probably
what is desired is \old(myVar.theStack).
To avoid such problems, it is good practice to have the expression E
in \old(E)
be such that its type is either the type of a primitive value,
such as an int, or a type with immutable objects,
such as JMLObjectSequence.
As another example, in pop's postcondition
the expression \old(theStack.trailer())
has type JMLObjectSequence, so it is immutable.
The value of theStack.trailer() is computed
in the pre-state of the method.
Note also that, since JMLObjectSequence is a reference type,
one is required to use equals instead of == to compare
them for equality of values.
(Using == would be a mistake, since it would only compare them
for object identity, which in combination with new would always
yield false.)
The specification of push does not have a requires
clause.
This means that the method imposes no obligations on the caller.
(The meaning of an omitted requires clause
is that the method's precondition is true, which
is satisfied by all states, and hence imposes no obligations on the caller.)
This seems to imply that the implementation must provide
a literally unbounded stack, which is surely impossible.
We avoid this problem, by following Poetzsch-Heffter [Poetzsch-Heffter97]
in releasing implementations from their obligations
to fulfill the postcondition when Java runs out of storage.
In general, a method specified with normal_behavior
has a correct implementation if,
whenever it is called in a state that satisfies
its precondition, either
assignable
clause, or
java.lang.Error.
We discuss the specification of methods with exceptions in the next subsection.
In specifying existing code, one often does not want to introduce new
model fields or think up new names for them. And sometimes,
especially for fields with simple, atomic values, the field name
itself is so "natural" that it would be difficult to think up a second
good name for a model field that would be an abstraction of it.
Thus JML provides two modifiers, spec_public and
spec_protected that can used to make existing fields public or
protected, for purposes of specification.
For example, consider the (lightweight) specification of the class
Point2D below. In this specification the private fields,
x and y are specified as spec_public, which
allows them to be used in the public invariant clause and in the
(implicitly public) specifications of the constructors and methods of
Point2D.
package org.jmlspecs.samples.prelimdesign;
//@ model import org.jmlspecs.models.JMLDouble;
public class Point2D
{
private /*@ spec_public @*/ double x = 0.0;
private /*@ spec_public @*/ double y = 0.0;
//@ public invariant !Double.isNaN(x) && !Double.isNaN(y);
//@ public invariant !Double.isInfinite(x) && !Double.isInfinite(y);
//@ ensures x == 0.0 && y == 0.0;
public Point2D() { }
/*@ requires !Double.isNaN(xc) && !Double.isNaN(yc);
@ requires !Double.isInfinite(xc) && !Double.isInfinite(yc);
@ assignable x, y;
@ ensures x == xc && y == yc;
@*/
public Point2D(double xc, double yc) {
x = xc;
y = yc;
}
//@ ensures \result == x;
public /*@ pure @*/ double getX() {
return x;
}
//@ ensures \result == y;
public /*@ pure @*/ double getY() {
return y;
}
/*@ requires !Double.isNaN(x+dx);
@ requires !Double.isInfinite(x+dx);
@ assignable x;
@ ensures JMLDouble.approximatelyEqualTo(x, \old(x+dx), 1e-10);
@*/
public void moveX(double dx) {
x += dx;
}
/*@ requires !Double.isNaN(y+dy);
@ requires !Double.isInfinite(y+dy);
@ assignable y;
@ ensures JMLDouble.approximatelyEqualTo(y, \old(y+dy), 1e-10);
@*/
public void moveY(double dy) {
y += dy;
}
}
Note that these specifications would be illegal without the use of
spec_public, since JML requires that public specifications can only
mention publicly-visible names
(see section 1.1 Behavioral Interface Specification).
However, spec_public is more than just a way to change the
visibility of a name for specification purposes. When applied to
fields it can be considered to be shorthand for the declaration of a
model field with the same name. That is, the declaration of x
in Point2D can be thought of as equivalent to the following
declarations, together with a rewrite of the Java code that uses x to
use _x instead (where we assume _x is not used elsewhere).
//@ public model int x; private int _x; //@ in x; //@ private represents x <- _x;
So in this way of thinking spec_public is not
just an access modifier, but shorthand for declaration of a model
field. This model field declaration is a commitment to readers that
they can understand the specification using these model fields, even
if the underlying private fields are changed, just as if the model
field were declared explicitly.
The model fields that are implicit allow such changes to be made with
affecting the readers of the specification.
For example, suppose one wanted to change the implementation of
Point2D, to use polar coordinates.
To do that while keeping the public specification
unchanged, one would declare the model fields x and y
explicitly. One would then declare other fields for the polar and
rectangular coordinates (and perhaps additional model fields as well).
One would then also need to give explicit declarations that the new
concrete fields are members of the model fields data groups, and give
appropriate represents clauses.
(See section 2.2.2.1 Data Groups and Represents Clauses, for more on data group
membership and represents clauses.)
All of this is exactly analogous to what is done implicitly in the the
desugaring described above.
Similar remarks apply to spec_protected. The
spec_public and spec_protected shorthands were borrowed
from ESC/Java, but the desugaring described above is novel with JML.
In this subsection we present two example specifications.
The two example specifications,
BoundedThing and BoundedStackInterface,
are used to describe how model (and concrete) fields can be related
to one another, and how dependencies among them affect the meaning
of the assignable clause.
Along the way we also demonstrate how to specify methods
that can throw exceptions and other features of JML.
The specification in the file `BoundedThing.java',
shown below, is an interface specification
with a simple abstract model.
In this case, there are two model fields MAX_SIZE
and size.
package org.jmlspecs.samples.stacks;
public interface BoundedThing {
//@ public model instance int MAX_SIZE;
//@ public model instance int size;
/*@ public instance invariant MAX_SIZE > 0;
public instance invariant
0 <= size && size <= MAX_SIZE;
public instance constraint MAX_SIZE == \old(MAX_SIZE);
@*/
/*@ public normal_behavior
ensures \result == MAX_SIZE;
@*/
public /*@ pure @*/ int getSizeLimit();
/*@ public normal_behavior
ensures \result <==> size == 0;
@*/
public /*@ pure @*/ boolean isEmpty();
/*@ public normal_behavior
ensures \result <==> size == MAX_SIZE;
@*/
public /*@ pure @*/ boolean isFull();
/*@ also
public behavior
assignable \nothing;
ensures \result instanceof BoundedThing
&& size == ((BoundedThing)\result).size;
signals (CloneNotSupportedException) true;
@*/
public Object clone () throws CloneNotSupportedException;
}
After discussing the model fields, we describe the other parts of the specification below.
In the specification above,
the fields MAX_SIZE and size
are both declared using the modifier instance.
Because of the use of the keyword instance,
these fields are thus treated as normal model fields,
i.e., as an instance variable in each object that implements this interface.
By default, as in Java, fields are static in interfaces,
and so if instance is omitted, the field declarations
would be treated as class variables.
The instance keyword tells the reader
that the variable being declared is not
static, but has a copy in each instance of a class that implements this
interface.
Java does not allow non-static fields to be declared in interfaces.
However, JML allows non-static model (and ghost) fields in interfaces
when one uses instance.
The reason for this extension is that such fields
are essential for defining the abstract values and behavior of
the objects being specified.(12)
In specifications of interfaces that extend
or classes that implement this interface,
these model fields are inherited.
Thus, every object that has a type that is a subtype of the
BoundedThing interface is thought of, abstractly,
as having two fields, MAX_SIZE and size,
both of type int.
Three pieces of class-level specification come after the abstract model in the above specification.
The first two are invariant clauses.
Writing several invariant clauses in a specification, like this
is equivalent to writing one invariant clause which is their
conjunction.
Both of these invariants are instance invariants,
because they use the instance modifier.
By default, in interfaces, invariants and history constraints are
static, unless marked with the instance modifier.
Static invariants may only refer to static fields, while instance
invariants can refer to both instance and static fields.
The first invariant in the figure says that in every publicly visible state,
every reachable object that is a BoundedThing
must have a positive MAX_SIZE field.
The second invariant says that, in each publicly visible state,
every reachable object that is a BoundedThing must have a size
field that is non-negative and less than or equal to MAX_SIZE.
Following the invariants is a history constraint [Liskov-Wing94].
Like the invariants, it uses the modifier instance,
because it refers to instance fields.
A history constraint is used to say how values can change between earlier
and later publicly-visible states,
such as a method's pre-state and its post-state.
This prohibits subtype objects from making certain state changes, even
if they implement more methods than are specified in a given class.
The history constraint in the specification above
says that the value of MAX_SIZE cannot change,
since in every pre-state and post-state, its value in the post-state,
written MAX_SIZE, must equal its value in the pre-state,
written \old(MAX_SIZE).
Following the history constraint are the interfaces and specifications
for four public methods. Notice that, if desired,
the at-signs (@) may be omitted from the left sides
of intermediate lines, as we do in this specification.
The use of == in the method specifications
is okay, since in each case, the things being compared are primitive values,
not references.
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"
in the postcondition of the isEmpty method means the same
thing as "\result == (size == 0)".
The specification of the last method of BoundedThing,
clone, is interesting.
Note that it begins with the keyword also.
This form is intended to tell the reader that the specification given is
in addition to any specification that might have been given in the superclass
Object, where clone is declared as a protected
method.
A form like this must be used whenever a specification is given for a
method that overrides a method in a superclass, or that implements a
method from an implemented interface.
The specification of clone
also uses behavior instead of normal_behavior.
In a specification that starts this way, one can describe
not just the case where the execution returns normally, but also
executions where exceptions are thrown.
In such a specification, the conditions under
which exceptions can be thrown can be described by the predicate in the
signals clauses,(13)
and the conditions under which the method may return without throwing
an exception are described by the ensures clause.
In this specification, the clone
method may always throw the exception, because it only needs to make
the predicate "true" true to do so.
When the method returns normally, it must make the given postcondition
true.
In JML, a normal_behavior specification can be thought of as a
syntactic sugar for a behavior specification to which the
following clause is added [Raghavan-Leavens00].
signals (java.lang.Exception) false;
This formalizes the idea that a method with a normal_behavior
specification may not throw an exception
when the specification's precondition is satisfied.
JML also has a specification form exceptional_behavior,
which can be used to specify when a method may not return normally.
A specification that uses exceptional_behavior can be thought of as a
syntactic sugar for a behavior specification to which the
following clause is added [Raghavan-Leavens00].
ensures false;
This formalizes the idea that a method with a exceptional_behavior
specification may not return normally
when the specification's precondition is satisfied.
Thus, when the precondition of an such a specification case holds,
some exception must be thrown (unless the execution encounters an
error or is permitted to not return to the caller).
Since in the specification of clone, we want to allow the
implementation to make a choice between either returning normally or
throwing an exception, and we do not wish to distinguish the
preconditions under which each choice must be made,
we cannot use either of the more specialized
forms normal_behavior or exceptional_behavior.
Thus the specification of clone
demonstrates the somewhat unusual case when
the more general form of a behavior specification is needed.
The specification of clone also illustrates another
aspect the semantics of signals clauses.
This is that a signals clause only describes what must be true when
the exceptions it applies to are thrown; it does not constrain a
method's behavior with respect to exceptions that are not subtypes of
the exceptions named. For example, clone's specification
only says that a CloneNotSupportedException can always be
thrown;
it does not prohibit other exceptions
that are not subtypes of CloneNotSupportedException from being
thrown.
For example, clone could throw a NullPointerException.
In this sense the specification given is an underspecification, as it
permits other behaviors than those it describes.
To prohibit other exceptions from being thrown, one could
use a signals clause such as the following.
signals (Exception e) e instanceof CloneNotSupportedException;
This takes advantage of the fact that all (non-error) exceptions in
Java are subtypes of java.lang.Exception.
If clone were specified with such a signals clause, then, for
example it could not throw a NullPointerException.
Finally note that in the specification of clone,
the postcondition says that the result will be a BoundedThing
and that its size will be the same as the model field size.
The use of the cast in this postcondition is necessary,
since the type of \result is Object.
(This also adheres to our goal of using Java syntax and
semantics to the extent possible.)
Note also that the conjunct \result instanceof BoundedThing
"protects" the next conjunct [Leavens-Wing97a]
since if it is false the meaning of the cast does not matter.
The specification in the file `BoundedStackInterface.java' below
gives an interface for bounded stacks
that extends the interface for BoundedThing.
Note that this specification can refer to the instance fields
MAX_SIZE and size inherited from the
BoundedThing interface.
package org.jmlspecs.samples.stacks;
//@ model import org.jmlspecs.models.*;
public interface BoundedStackInterface extends BoundedThing {
//@ public initially theStack != null && theStack.isEmpty();
/*@ public model instance JMLObjectSequence theStack;
@ in size;
@*/
//@ public instance represents size <- theStack.int_length();
/*@ public instance invariant theStack != null;
@ public instance invariant_redundantly
@ theStack.int_length() <= MAX_SIZE;
@ public instance invariant
@ (\forall int i; 0 <= i && i < theStack.int_length();
@ theStack.itemAt(i) != null);
@*/
/*@ public normal_behavior
@ requires !theStack.isEmpty();
@ assignable size, theStack;
@ ensures theStack.equals(\old(theStack.trailer()));
@ also
@ public exceptional_behavior
@ requires theStack.isEmpty();
@ assignable \nothing;
@ signals (BoundedStackException);
@*/
public void pop( ) throws BoundedStackException;
/*@ public normal_behavior
@ requires theStack.int_length() < MAX_SIZE && x != null;
@ assignable size, theStack;
@ ensures theStack.equals(\old(theStack.insertFront(x)));
@ ensures_redundantly theStack != null && top() == x
@ && theStack.int_length() == \old(theStack.int_length()+1);
@ also
@ public exceptional_behavior
@ requires theStack.int_length() >= MAX_SIZE || x == null;
@ assignable \nothing;
@ signals (BoundedStackException)
@ theStack.int_length() == MAX_SIZE;
@ signals (NullPointerException) x == null;
@*/
public void push(Object x )
throws BoundedStackException, NullPointerException;
/*@ public normal_behavior
@ requires !theStack.isEmpty();
@ ensures \result == theStack.first() && \result != null;
@ also
@ public exceptional_behavior
@ requires theStack.isEmpty();
@ signals (BoundedStackException e)
@ \fresh(e) && e != null && e.getMessage() != null
@ && e.getMessage().equals("empty stack");
@ signals_redundantly (BoundedStackException);
@*/
public /*@ pure @*/ Object top( ) throws BoundedStackException;
}
The abstract model for BoundedStackInterface adds to the inherited
model by declaring a model instance field named theStack.
This field is typed as a JMLObjectSequence.
In the following we describe how the new model instance field,
theStack, is related to size from BoundedThing.
We also use this example to explain more JML features.
The in and represents clauses
that follow the declaration of theStack
are an important feature in modeling
with layers of model fields.(14)
They also play a crucial role in relating model fields
to the concrete fields of objects,
which can be considered to be the final layer of detail in a design.
When a model field is declared, a data group with the same name is automatically created; furthermore, this field is always a member of the group it creates. A data group is a set of fields (locations) referenced by a specific name, i.e., the name of the model field that created it [Leino98] [Leino-Poetzsch-Heffter-Zhou02].
When a data group (or field) is mentioned in the assignable clause
for a method M, then all members (i.e., fields) in that group
can be assigned to in the body of M.
Fields can become a member of a data group through the
data group clauses (i.e., the in and maps-into clauses) that
come immediately after the field declaration, in this case
the in clause.
The in clause in BoundedStackInterface
says that theStack is a member of the group created by
the declaration of model field size;
this means that theStack
might change its value whenever size changes.
However, another way of looking at this is that,
if one wants to change size, this can be done by
changing theStack.
We also say that theStack is a member of size.
The maps-into clause is another way of adding members to a data
group; it allows the fields of an object to
be included in an existing data group.
For example, if a field F is a reference or an array type,
then the fields or array elements of F can be included in a
data group using the maps-into clause.
The following are examples.
protected ArrayList elems; //@ maps elems.theList \into theStack; protected java.lang.Object[] theItems; //@ maps theItems[*] \into theStack;
In the first example, the maps-into clause says that
theList field of
elems is a member of theStack data group.
Field elems is a concrete field of the type
(i.e., it is not a model field and thus is part of the implementation).
This allows model field theList of elems to change when
theStack changes.
Since theList is a model field and data group, this also allows
concrete fields of elems to change as theStack changes.
Similarly, the second example says that the elements of the array
theItems can change when theStack changes.
Data groups have the same visibility as the model field that declared it, i.e, public, protected, private, or package visibility. A field cannot be a member of a group that is less visible than it is. For example, a public field cannot be a member of a protected group.
The in and maps-into clauses are important in "loosening up"
the assignable clause, for example to permit the fields of an object
that implement the abstract model to be changed
[Leino95] [Leino95a].
This "loosening up" also applies to model fields
that are members of other groups.
For example, since theStack is a member of size,
whenever size is mentioned in an assignable clause,
then theStack is implicitly allowed to be modified.(15)
Thus it is only for rhetorical purposes that
we mention both size and theStack
in the assignable clauses of pop and push.
Note, however, that just mentioning theStack would not permit
size to be modified, because size is not a member of
theStack's group.
Furthermore, it is redundant to mention theStack when
size has already been mentioned (although this can help clarify
the assignable clause, i.e., clarify which fields can be changed).
The represents clause in BoundedStackInterface
says how the value of size is related
to the value of theStack.
It says that the value of size is theStack.length().
A represents clause gives additional facts that can be used in reasoning about the specification. It serves the same purpose as an abstraction function in various proof methods for abstract data types (such as [Hoare72a]).
One can only use a represents clause to state facts about a field and its data group members. To state relationships among concrete data fields or on fields that are not related by a data group membership, one should use an invariant.
The second invariant clause
that follows the represents clause
in the specification of BoundedStackInterface above
is our first example of checkable redundancy in a specification
[Leavens-Baker99] [Tan94] [Tan95].
This concept is signaled in JML by the use of the suffix _redundantly
on a keyword (as in ensures_redundantly).
It says both that the stated property is specified to hold
and that this property is believed to follow from the other
properties of the specification.
In this case the redundant invariant follows from the given invariant,
the invariant inherited from the specification of BoundedThing,
and the fact stated in the represents clause.
Even though this invariant is redundant,
it is sometimes helpful to state such properties, to bring them
to the attention of the readers of the specification.
Checking that such claimed redundancies really do follow from other information is also a good way to make sure that what is being specified is really what is intended. Such checks could be done manually, during reviews, or with the aid of a theorem prover. JML's runtime assertion checker can also check such redundant specifications, but, of course, can only find examples where they do not hold.
Following the redundant invariant of BoundedStackInterface
are the specifications of
the pop, push, and top methods.
These are interesting for several new features that they present.
Each of these has both a normal and exceptional behavior specified.
The meaning of such multiple specification cases is that,
when the precondition of one of them is satisfied,
the rest of that specification case must also be obeyed.
A specification with several specification cases
is shorthand for one in which the
separate specifications are combined
[Dhara-Leavens96] [Leavens97c] [Wing83] [Wills94].
The desugaring can be thought of as proceeding in two steps
(see [Raghavan-Leavens00] for more details).
First, the public normal_behavior and public exceptional_behavior
cases are converted into public behavior specifications as explained above.
This would produce a specification for pop as shown below.
The use of implies_that introduces a redundant specification
that can be used, as is done here,
to point out consequences of the specification to the reader.
In this case the specification in question is the one mentioned in the
refine clause.
Note that in the second specification case of the figure below,
the signals clause has been expanded to include the implicit predicate
"true";
this "true" was omitted from the original specification,
since such a use of the signals clause is common enough for
JML to allow it to be omitted.
//@ refine "BoundedStackInterface.java";
public interface BoundedStackInterface extends BoundedThing {
/*@ also
@ implies_that
@ public behavior
@ requires !theStack.isEmpty();
@ assignable size, theStack;
@ ensures theStack.equals(\old(theStack.trailer()));
@ signals (java.lang.Exception) false;
@ also
@ public behavior
@ requires theStack.isEmpty();
@ assignable \nothing;
@ ensures false;
@ signals (BoundedStackException) true;
@*/
public void pop( ) throws BoundedStackException;
}
The second step of the desugaring is shown
below.
As can be seen from this example,
public behavior specifications that are joined together using also
have a precondition that is the disjunction of the preconditions
of the combined specification cases.
The assignable clause for the expanded specification
is the union of all the assignable clauses for the cases,
with each modification governed by the corresponding precondition
(which follows the keyword if).
That is, variables are only allowed to be modified if the modification
was permitted in the corresponding case, as determined by its
precondition.
The ensures clauses of the second desugaring step correspond to
the ensures clauses for each specification case;
they say that whenever the precondition for that specification case held
in the pre-state, its postcondition must also hold.
As can be seen in the specification below,
in logic this is written using an implication between
\old wrapped around the case's precondition and its postcondition.
Having multiple ensures clauses is equivalent to writing
a single ensures clause that has as its postcondition the conjunction
of the given postconditions.
Similarly, the signals clauses in the desugaring correspond to
those in the given specification cases;
as for the ensures clauses, each has a predicate that
says that signaling that exception can only happen
when the predicate in that case's precondition holds.
//@ refine "BoundedStackInterface.jml";
public interface BoundedStackInterface extends BoundedThing {
/*@ also
@ implies_that
@ public behavior
@ requires !theStack.isEmpty() || theStack.isEmpty();
@ assignable size, theStack;
@ ensures \old(!theStack.isEmpty())
@ ==> theStack.equals(\old(theStack.trailer()));
@ ensures \old(theStack.isEmpty()) ==>
@ \not_assigned(size) && \not_assigned(theStack);
@ signals (java.lang.Exception)
@ \old(!theStack.isEmpty()) ==> false;
@ signals (BoundedStackException)
@ \old(theStack.isEmpty()) ==> true;
@*/
public void pop( ) throws BoundedStackException;
}
In the file `BoundedStackInterface.refines-java' above,
the precondition of pop reduces to true.
However, the precondition shown is the general form of the expansion.
Similar remarks apply to other predicates.
Finally, note how, as in the specification of top,
one can specify more details about the exception object thrown.
The exceptional behavior for top says that the exception object
thrown, e, must be freshly allocated, non-null, and have the
given message.
A particularly interesting example of multiple specification cases occurs
in the specification of the BoundedStackInterface's push method.
Like the other methods, this example has two specification cases;
one of these is a normal_behavior
and one is an exceptional_behavior.
However, the exceptional behavior of push is interesting
because it specifies more than one exception that may be thrown.
The requires clause of the exceptional behavior says that
an exception must be thrown when either the stack cannot grow larger,
or when the argument x is null.
The first signals clause says that, if a BoundedStackException
is thrown, then the stack cannot grow larger,
and the second signals clause says that, if a NullPointerException
is thrown, then x must be null.
The specification is written in this way because it may be that
both conditions occur;
when that is the case, the specification allows the implementation to choose
(even nondeterministically) which exception is thrown.
Specifiers should be wary of such situations, where two different
signals clauses may both apply simulataneously, because it is impossible in
Java to throw more than one exception from a method call. Thus, for
example, if the specification of push had been written as
follows, it would not be implementable.(16)
The problem is that both exceptional preconditions may be true,
and in that case an implementation cannot throw an exception that is
an instance of both a BoundedStackException and a
NullPointerException.
/*@ public normal_behavior
@ requires theStack.length() < MAX_SIZE && x != null;
@ assignable size, theStack;
@ ensures theStack.equals(\old(theStack.insertFront(x)));
@ ensures_redundantly theStack != null && top() == x
@ && theStack.length() == \old(theStack.length()+1);
@ also
@ public exceptional_behavior
@ requires theStack.length() >= MAX_SIZE;
@ assignable \nothing;
@ signals (Exception e) e instanceof BoundedStackException;
@ also // this is wrong!
@ public exceptional_behavior
@ requires x == null;
@ assignable \nothing;
@ signals (Exception e) e instanceof NullPointerException;
@*/
public void push(Object x )
throws BoundedStackException, NullPointerException;
One could fix the example above by writing one of the requires clauses in the two exceptional behaviors to exclude the other, although this would make the specification deterministic about which exception would be thrown when both exceptional conditions occur. In general, it seems best to avoid this pitfall by writing signals clauses that do not exclude other exceptions from being thrown whenever there are states in which multiple exceptions may be thrown. That is, instead of using a signals clause like:
signals (Exception e) e instanceof BoundedStackException;
which only allows a BoundedStackException to be thrown when the
precondition is true, one can write a signals clause like:
signals (BoundedStackException);
which says nothing about what happens when other exceptions are thrown (see section 2.2.1.5 Specifying Exceptional Behavior for more details).
Finally, there is more redundancy in the specifications of push
in the original specification of BoundedStackInterface above,
which has a redundant ensures clause in its normal behavior.
For an ensures_redundantly clause,
what one checks is that the conjunction
of the precondition, the meaning of the assignable clause, and the
(non-redundant) postcondition together imply the redundant postcondition.
It is interesting to note that,
for push, the specifications for stacks written in
Eiffel (see page 339 of [Meyer97]) expresses just what we specify
in push's redundant postcondition.
This conveys strictly less information than the non-redundant
postcondition for push's normal behavior,
since it says little about the elements of the stack.(17)
JML comes with a suite of types with immutable objects and pure
methods, that can be used for defining abstract models.
These are found in the package
org.jmlspecs.models,
which includes both collection and non-collection types
(such as JMLInteger)
and a few auxiliary classes (such as exceptions and enumerators).
The collection types in this package can hold either objects or values;
this distinction determines the notion of equality used on their
elements and whether cloning is done on the elements.
The object collections, such as JMLObjectSet
and JMLObjectBag, use == and do not clone.
The value collections, such as JMLValueSet
and JMLValueBag, use .equals to compare elements,
and clone the objects added to and returned from them.
The objects in a value collection are representatives of equivalence
classes (under .equals) of objects; their values matter, but not
their object identities. By contrast an object container contains
object identities, and the values in these objects do not matter.
Simple collection types include
the set types, JMLObjectSet and JMLValueSet,
and sequence types JMLObjectSequence and JMLValueSequence.
The binary relation and map types can independently have objects in their
domain or range.
The binary relation types are named
JMLObjectToObjectRelation, JMLObjectToValueRelation,
and so on.
For example, JMLObjectToValueRelation is a type of binary
relations between objects (not cloned and compared using ==)
and values (which are cloned and compared using .equals).
The four map types are similarly named according to the scheme
JML...To...Map.
Users can also create their own types with pure methods for
mathematical modeling if desired.
Since pure methods may be used in assertions,
they must be declared with the modifier pure
and pass certain conservative checks that make sure there is no
possibility of observable side-effects from their use.
We discuss purity and give several examples of such types below.
We say a method
is pure if it is either specified with
the modifier pure or is a non-static method that
appears in the specification of a pure interface or class.
Similarly, a constructor is pure if it is either specified with
the modifier pure or appears in the specification of a pure
class.
A pure method that is not a constructor implicitly has a specification that does not allow any side-effects. That is, its specification refines (i.e., is stronger than) the following(18):
behavior
assignable \nothing;
A pure constructor implicitly has a specification that only allows it to assign to the non-static fields of the class in which it appears (including those inherited from its superclasses and model instance fields from the interfaces that implements).
Implementations of pure methods and constructors will be checked to see that they meet these conditions on what locations they can assign to. To make such checking modular, a pure method or constructor implementation is prohibited from calling methods or constructors that are not pure.
A pure method or constructor must also be provably terminating.(19)
Recursion is permitted, both in the implementation of pure methods
and the data structures they manipulate, and in the specifications of
pure methods.
When recursion is used in a specification,
the proof of well-formedness for the specification
involves the use of JML's measured_by clause.
Since a pure method may not go into an infinite loop, if it has a non-trivial precondition, it should throw an exception when its normal precondition is not met. This exceptional behavior does not have to be specified or programmed explicitly, but technically there is an obligation to meet the specification that the method never loops forever.
A pure method can be declared in any class or interface, and a pure constructor can be declared in any class. JML will specify the pure methods and constructors in the standard Java libraries as pure.
As a convenience, instead of writing pure on each
method declared in a class and interface,
one can use the modifier pure on classes and
interfaces and classes.
This simply means that each non-static method and each constructor
declared in such a class or interface is pure.
Note that this does not mean that all methods inherited (but not
declared in and hence not overridden in) the class or interface are
pure.
For example, every class inherits ultimately from
java.lang.Object,
which has some methods, such as notify and notifyAll
that are manifestly not pure.
Thus each class will have some methods that are not pure.
Despite this, it is convenient to refer to classes and interfaces declared
with the pure modifier as pure.
In JML the modifiers model and pure
are orthogonal. (Recall something declared with
the modifier model does not have to be
implemented, and is used purely for specification purposes.)
Therefore, one can have a model method
that is not pure (these might be useful in JML's model programs)
and a pure method that is not a model method.
Nevertheless, usually a model method (or constructor) should be pure,
since there is no way to use non-pure methods in an assertion,
and model methods cannot be used in normal Java code.
By the same reasoning, model classes should, in general, also be pure. Model classes cannot be used in normal Java code, and hence their methods are only useful in assertions (and JML's model programs). Hence it is typical, although not required, that a model class also be a pure class. We give some examples of pure interfaces, abstract classes, and classes below.
The following example begins a specification of money that would be suitable for use in abstract models. Our specification is rather artificially broken up into pieces to allow each piece to have a specification that fits on a page. This organization is not necessarily something we would recommend, but it does give us a chance to illustrate more features of JML.
Consider first the interface Money
specified below.
The abstract model here is a single field
of the primitive Java type long,
which holds a number of pennies.
Note that the declaration of this field, pennies,
again uses the JML keyword instance.
package org.jmlspecs.samples.prelimdesign;
import org.jmlspecs.models.JMLType;
public /*@ pure @*/ interface Money extends JMLType
{
//@ public model instance long pennies;
//@ public instance constraint pennies == \old(pennies);
/*@ public normal_behavior
@ assignable \nothing;
@ ensures \result == pennies / 100;
@ for_example
@ public normal_example
@ requires pennies == 703;
@ assignable \nothing;
@ ensures \result == 7;
@ also
@ public normal_example
@ requires pennies == 799;
@ assignable \nothing;
@ ensures \result == 7;
@ also
@ public normal_example
@ requires pennies == -503;
@ assignable \nothing;
@ ensures \result == -5;
@*/
public long dollars();
/*@ public normal_behavior
@ assignable \nothing;
@ ensures \result == pennies % 100;
@ for_example
@ requires pennies == 703;
@ assignable \nothing;
@ ensures \result == 3;
@ also
@ requires pennies == -503;
@ assignable \nothing;
@ ensures \result == -3;
@*/
public long cents();
/*@ also
@ public normal_behavior
@ assignable \nothing;
@ ensures \result <==> o2 instanceof Money
@ && pennies == ((Money)o2).pennies;
@*/
public boolean equals(Object o2);
/*@ also
@ public normal_behavior
@ assignable \nothing;
@ ensures \result instanceof Money
@ && ((Money)\result).pennies == pennies;
@*/
public Object clone();
}
This interface has a history constraint, which says that the number of pennies in an object cannot change.(20)
The following explain more aspects of JML related to the above specification.
The interesting aspect of Money's method specifications is another kind of redundancy.
This new form of redundancy is examples,
which follow the keyword "for_example".
Individual examples
are given by normal_example clauses
(adapted from our previous work on Larch/C++ [Leavens96b] [Leavens-Baker99]).
Any number of these(21)
can be given in a specification.
In the specification of Money above
there are three normal examples given for dollars
and two in the specification of cents.
The specification in each example should be such that:
\old()),
the precondition of the expanded meaning of the specified behaviors
(also wrapped by \old()),
the assignable clause of the expanded meaning of the specified behaviors,
and the postcondition of the expanded meaning of the specified behaviors
should be equivalent to
the conjunction of the assignable clause of the expanded meaning
of the example
and
the example's postcondition.
Requiring equivalence to the example's postcondition
means that it can serve as a test oracle for the
inputs described by the example's precondition.
If there is only one specified public normal_behavior clause
and if there are no preconditions and assignable clauses,
then the example's postcondition should the equivalent to
the conjunction of the example's precondition
and the postcondition of the public normal_behavior specification.
Typically, examples are concrete, and serve to make various rhetorical
points about the use of the specification to the reader.
(Exercise: check all the examples given!)
The interface Money is specified to extend the interface
JMLType.
This interface is given below.
Classes that implement this interface must
have pure equals and clone methods
with the specified behavior.
The methods specified override methods in the class
Object, and so they use the form of specification
that begins with the keyword "also".
package org.jmlspecs.models;
/** Objects with a clone and equals method.
* JMLObjectType and JMLValueType are refinements
* for object and value containers (respectively).
* @version $Revision: 1.14 $
* @author Gary T. Leavens
* @author Albert L. Baker
* @see JMLObjectType
* @see JMLValueType
*/
//@ pure
public interface JMLType extends Cloneable, java.io.Serializable {
/** Return a clone of this object.
*/
/*@ also
@ public normal_behavior
@ ensures \result != null;
@ ensures \result instanceof JMLType;
@ ensures ((JMLType)\result).equals(this);
@*/
//@ implies_that
/*@ ensures \result != null
@ && \typeof(\result) <: \type(JMLType);
@*/
public /*@ pure @*/ Object clone();
/** Test whether this object's value is equal to the given argument.
*/
/*@ also
@ public normal_behavior
@ ensures \result ==>
@ ob2 != null
@ && (* ob2 is not distinguishable from this,
@ except by using mutation or == *);
@ implies_that
@ public normal_behavior
@ {|
@ requires ob2 != null && ob2 instanceof JMLType;
@ ensures ((JMLType)ob2).equals(this) == \result;
@ also
@ requires ob2 == this;
@ ensures \result <==> true;
@ |}
@*/
public /*@ pure @*/ boolean equals(Object ob2);
/** Return a hash code for this object.
*/
public /*@ pure @*/ int hashCode();
}
The specification of JMLType
is noteworthy in its use of informal predicates [Leavens96b].
In JML these start with an open parenthesis and an asterisk (`(*')
and continue until a matching asterisk and closing parenthesis (`*)').
In the public specification of equals,
the normal_behavior's ensures clause
uses an informal predicate as an escape from formality.
The use of informal predicates avoids the delicate issues of saying
formally what observable aliasing means,
and what equality of values means in general.(22)
In the implies_that section of the specification of the
equals method is a nested case analysis, between {|
and |}. The meaning of this is that each pre- and postcondition
pair has to be obeyed. The first of these nested pairs is essentially
saying that equals has to be symmetric. The second of these is
saying that it has to be reflexive.
The implies_that section of the clone method states
some implications of the specification given that are useful for
ESC/Java. These repeat, from the first part of clone's
specification, that the result must not be null, and that
the result's dynamic type, \typeof(\result),
must be a subtype of (written <:) the type JMLType.
ESC/Java understands only annotations written between the annotation
markers /*@ and @*/ and on annotation comment lines of
that start with //@.
It does not understand annotations written between the annotation
markers /*+@ and @+*/ and on annotation comment lines of
that start with //+@.(23)
This makes it possible for the user of JML to write specifications
that can be read by both JML's tools and by ESC/Java,
since JML understands (essentially) a superset of the syntax that
ESC/Java understands.
The type Money lacks some useful operations.
The extensions below
provide specifications of comparison operations and arithmetic, respectively.
The specification in file `MoneyComparable.java' is interesting because
each of the specified preconditions protects the postcondition from
undefinedness in the postcondition [Leavens-Wing97a].
For example, if the argument m2 in the greaterThan
method were null, then the expression m2.pennies would
not be defined.
package org.jmlspecs.samples.prelimdesign;
public /*@ pure @*/ interface MoneyComparable extends Money
{
/*@ public normal_behavior
@ requires m2 != null;
@ assignable \nothing;
@ ensures \result <==> pennies > m2.pennies;
@*/
public boolean greaterThan(Money m2);
/*@ public normal_behavior
@ requires m2 != null;
@ assignable \nothing;
@ ensures \result <==> pennies >= m2.pennies;
@*/
public boolean greaterThanOrEqualTo(Money m2);
/*@ public normal_behavior
@ requires m2 != null;
@ assignable \nothing;
@ ensures \result <==> pennies < m2.pennies;
@*/
public boolean lessThan(Money m2);
/*@ public normal_behavior
@ requires m2 != null;
@ assignable \nothing;
@ ensures \result <==> pennies <= m2.pennies;
@*/
public boolean lessThanOrEqualTo(Money m2);
}
The interface specified in the file `MoneyOps.java'
below extends the interface specified above.
MoneyOps is interesting for
the use of its pure model methods: inRange,
can_add, and can_scaleBy.
These methods cannot be invoked by Java programs;
that is, they would not appear in the Java implementation.
When, for example inRange is called in a predicate it is
equivalent to using some correct implementation of its specification.
The specification of inRange also makes use of a local specification
variable declaration, which follows the keyword "old".
Such declarations allow one to abbreviate long expressions, or,
to make rhetorical points by naming constants,
as is done with epsilon.
These old declarations are treated as locations
that are initialized to the pre-state value of the given expression.
Model methods can be normal (instance) methods
as well as static (class) methods.
package org.jmlspecs.samples.prelimdesign;
public /*@ pure @*/ interface MoneyOps extends MoneyComparable
{
/*@ public normal_behavior
@ old double epsilon = 1.0;
@ assignable \nothing;
@ ensures \result <==> Long.MIN_VALUE + epsilon < d
@ && d < Long.MAX_VALUE - epsilon;
@ public model boolean inRange(double d);
@
@ public normal_behavior
@ requires m2!= null;
@ assignable \nothing;
@ ensures \result <==> inRange((double) pennies + m2.pennies);
@ public model boolean can_add(Money m2);
@
@ public normal_behavior
@ ensures \result <==> inRange(factor * pennies);
@ public model boolean can_scaleBy(double factor);
@*/
/*@ public normal_behavior
@ requires m2 != null && can_add(m2);
@ assignable \nothing;
@ ensures \result != null
@ && \result.pennies == this.pennies + m2.pennies;
@ for_example
@ public normal_example
@ requires this.pennies == 300 && m2.pennies == 400;
@ assignable \nothing;
@ ensures \result != null && \result.pennies == 700;
@*/
public MoneyOps plus(Money m2);
/*@ public normal_behavior
@ requires m2 != null
@ && inRange((double) pennies - m2.pennies);
@ assignable \nothing;
@ ensures \result != null
@ && \result.pennies == this.pennies - m2.pennies;
@ for_example
@ public normal_example
@ requires this.pennies == 400 && m2.pennies == 300;
@ assignable \nothing;
@ ensures \result != null && \result.pennies == 100;
@*/
public MoneyOps minus(Money m2);
/*@ public normal_behavior
@ requires can_scaleBy(factor);
@ assignable \nothing;
@ ensures \result != null
@ && \result.pennies == (long)(factor * pennies);
@ for_example
@ public normal_example
@ requires pennies == 400 && factor == 1.01;
@ assignable \nothing;
@ ensures \result != null && \result.pennies == 404;
@*/
public MoneyOps scaleBy(double factor);
}
Note also that JML uses the Java semantics for mixed-type expressions.
For example in the ensures clause of the above specification of plus,
m2.pennies is implicitly coerced to a double-precision floating point number,
as it would be in Java.
The key to proofs that an implementation of a class or interface
specification is correct lies in the use of in, maps-into,
and represents clauses [Hoare72a] [Leino95].
Consider, for example, the abstract class
specified in the file `MoneyAC.java' below.
This class is abstract and has no constructors.
The class declares a concrete field numCents,
which is related to the model instance field pennies
by the represents clause.(24)
The represents clause states that the value of pennies
is the value of numCents.
This allows relatively trivial proofs of the correctness of the
dollars and cents methods, and is key to the proofs
of the other methods.
package org.jmlspecs.samples.prelimdesign;
public /*@ pure @*/ abstract class MoneyAC implements Money {
protected long numCents;
//@ in pennies;
//@ protected represents pennies <- numCents;
//@ protected constraint_redundantly numCents == \old(numCents);
public long dollars() {
return numCents / 100;
}
public long cents() {
return numCents % 100;
}
public boolean equals(Object o2) {
if (o2 instanceof Money) {
Money m2 = (Money)o2;
return numCents == (100 * m2.dollars() + m2.cents());
} else {
return false;
}
}
public int hashCode() {
return (int)numCents;
}
public Object clone() {
return this;
}
}
The straightforward implementation of the pure abstract subclass
MoneyComparableAC is given below.
Besides extending the class MoneyAC,
it implements the interface MoneyComparable.
Note that the model and concrete fields are both inherited
by this class.
package org.jmlspecs.samples.prelimdesign;
public /*@ pure @*/ abstract class MoneyComparableAC
extends MoneyAC implements MoneyComparable
{
protected static /*@ pure @*/ long totalCents(Money m2)
{
long res = 100 * m2.dollars() + m2.cents();
//@ assert res == m2.pennies;
return res;
}
public boolean greaterThan(Money m2)
{
return numCents > totalCents(m2);
}
public boolean greaterThanOrEqualTo(Money m2)
{
return numCents >= totalCents(m2);
}
public boolean lessThan(Money m2)
{
return numCents < totalCents(m2);
}
public boolean lessThanOrEqualTo(Money m2)
{
return numCents <= totalCents(m2);
}
}
An interesting feature of the class MoneyComparableAC
is the protected static method named totalCents.
For this method, we give its code with an embedded assertion,
written following the keyword assert.(25)
Note that the model method, inRange is not implemented,
and does not need to be implemented to make this class correctly implement
the interface MoneyComparable.
Finally, a concrete class implementation
is given in the file `USMoney.java' shown below.
The class USMoney implements the interface MoneyOps.
Note that specifications as well as code are given for the constructors.
package org.jmlspecs.samples.prelimdesign;
public /*@ pure @*/ class USMoney
extends MoneyComparableAC implements MoneyOps
{
/*@ public normal_behavior
@ assignable pennies;
@ ensures pennies == cs;
@ implies_that
@ protected normal_behavior
@ assignable pennies, numCents;
@ ensures numCents == cs;
@*/
public USMoney(long cs)
{
numCents = cs;
}
/*@ public normal_behavior
@ assignable pennies;
@ ensures pennies == (long)(100.0 * amt);
@ ensures_redundantly (* pennies holds amt dollars *); @*/
public USMoney(double amt)
{
numCents = (long)(100.0 * amt);
}
public MoneyOps plus(Money m2)
{
//@ assume m2 != null;
return new USMoney(numCents + totalCents(m2));
}
public MoneyOps minus(Money m2)
{
//@ assume m2 != null;
return new USMoney(numCents - totalCents(m2));
}
public MoneyOps scaleBy(double factor)
{
return new USMoney(numCents * factor / 100.0);
}
public String toString()
{
return "$" + dollars() + "." + cents();
}
}
The constructors each mention the fields that they initialize
in their assignable clause.
This is because the constructor's job is to initialize these fields.
One can think of a new expression in Java as executing
in two steps: allocating an object, and then calling the constructor.
Thus the specification of a constructor needs to mention the fields
that it can initialize in the assignable clause.
The first constructor's specification also illustrates that redundancy
can also be used in an assignable clause.
A redundant assignable clause follows
if the meaning of the set of locations named is a subset of the
ones denoted by the non-redundant clause for the same specification case.
In this example
the redundant assignable clause follows from the given assignable
clause and the meaning of the in clause inherited from the
superclass MoneyAC.
The second constructor above is noteworthy in that there is a redundant ensures clauses that uses an informal predicate [Leavens96b]. In this instance, the informal predicate is used as a comment (which could also be used). Recall that informal predicates allow an escape from formality when one does not wish to give part of a specification in formal detail.
The plus and minus methods use assume statements;
these are like assertions, but are intended to impose obligations
on the callers [Back-Mikhajlova-vonWright98].
The main distinction between a assume statement and a requires
clause is that the former is a statement and can be used within code.
These may also be treated differently by different tools.
For example, ESC/Java [Leino-etal00]
will require callers to satisfy the requires clause of a method,
but will not enforce the precondition if it is stated as an assumption.
Since USMoney is a pure class,
it can be used to make models of other classes.
An example is the abstract class specified in the file
`Account.jml' below.
The first model field in this class has the type USMoney,
which was specified above.
(Further explanation follows the specification below.)
package org.jmlspecs.samples.prelimdesign;
public class Account {
//@ public model MoneyOps credit;
//@ public model String accountOwner;
/*@ public invariant accountOwner != null && credit != null
@ && credit.greaterThanOrEqualTo(new USMoney(0));
@*/
//@ public constraint accountOwner.equals(\old(accountOwner));
/*@ public normal_behavior
@ requires own != null && amt != null
@ && (new USMoney(1)).lessThanOrEqualTo(amt);
@ assignable credit, accountOwner;
@ ensures credit.equals(amt) && accountOwner.equals(own);
@*/
public Account(MoneyOps amt, String own);
/*@ public normal_behavior
@ assignable \nothing;
@ ensures \result.equals(credit);
@*/
public /*@ pure @*/ MoneyOps balance();
/*@ public normal_behavior
@ requires 0.0 <= rate && rate <= 1.0
@ && credit.can_scaleBy(1.0 + rate);
@ assignable credit;
@ ensures credit.equals(\old(credit.scaleBy(1.0 + rate)));
@ for_example
@ public normal_example
@ requires rate == 0.05 && (new USMoney(4000)).equals(credit);
@ assignable credit;
@ ensures credit.equals(new USMoney(4200));
@*/
public void payInterest(double rate);
/*@ public normal_behavior
@ requires amt != null
@ && amt.greaterThanOrEqualTo(new USMoney(0))
@ && credit.can_add(amt);
@ assignable credit;
@ ensures credit.equals(\old(credit.plus(amt)));
@ for_example
@ public normal_example
@ requires credit.equals(new USMoney(40000))
@ && amt.equals(new USMoney(1));
@ assignable credit;
@ ensures credit.equals(new USMoney(40001));
@*/
public void deposit(MoneyOps amt);
/*@ public normal_behavior
@ requires amt != null && (new USMoney(0)).lessThanOrEqualTo(amt)
@ && amt.lessThanOrEqualTo(credit);
@ assignable credit;
@ ensures credit.equals(\old(credit.minus(amt)));
@ for_example
@ public normal_example
@ requires credit.equals(new USMoney(40001))
@ && amt.equals(new USMoney(40000));
@ assignable credit;
@ ensures credit.equals(new USMoney(1));
@*/
public void withdraw(MoneyOps amt);
}
The specification of Account makes good use of examples.
It also demonstrates the various ways of protecting predicates used
in the specification from undefinedness [Leavens-Wing97a].
The principal concern here, as is often the case when using reference
types in a model, is to protect against the model fields being
null.
As in Java, fields and variables of reference types can be null.
In the specification of Account, the invariant states that these fields
should not be null.
Since implementations of public methods must preserve the invariants,
one can think of the invariant as conjoined to the precondition
and postcondition of each public method, and the postcondition of each
public constructor.
Hence, for example, method pre- and postconditions do not have
to state that the fields are not null.
However, often other parts of the specification must be written
to allow the invariant to be preserved, or established by a constructor.
For example, in the specification of Account's constructor,
this is done by requiring amt and own are not null,
since, if they could be null, then the invariant could not be established.
The following specifications lead to
the specification of a class Digraph (directed graph).
This gives a more interesting example of how
more complex models can be composed in JML from
other classes.
In this example we use model classes
and the pure containers provided in the package
org.jmlspecs.models.
The file `NodeType.java'
contains the specification of an abstract class NodeType.
NodeType is an abstract
class, as opposed to a model class, because it will require an
implementation and because it does appear in the interface of the model class
Digraph.
However, we also declare this abstract class to be pure,
since we want to use its methods in the specification of other classes. (And we
do so appropriately, since all the methods for class NodeType are
side-effect-free.)
package org.jmlspecs.samples.digraph;
import org.jmlspecs.models.*;
public /*@ pure @*/ abstract class NodeType implements JMLType {
/*@ also
@ public normal_behavior
@ requires !(o instanceof NodeType);
@ ensures \result == false;
@*/
public abstract boolean equals(Object o);
public abstract int hashCode();
/*@ also
@ public normal_behavior
@ ensures \result instanceof NodeType
@ && ((NodeType)\result).equals(this);
@*/
public abstract Object clone();
} // end of class NodeType
ArcType is specified as a
pure model class in the file `ArcType.jml' shown below.
It is a model class because it does not appear in the interface
to Digraph, and so does not need to be implemented.
We declare ArcType to be a pure class
so that its methods can be used in assertions.
The two model fields for ArcType,
from and to, are both
of type NodeType.
We specify the equals method so that two references
to objects of type ArcType are equal if and only if they have equal
values in the from and to model fields.
Thus, equals is specified using NodeType.equals.
We also specify that ArcType
has a public clone method,
fulfilling the obligations of a type that implements
JMLType.
ArcType must implement JMLType so that
its objects can be placed in a JMLValueSet.
We use such a set for one of the model fields of Digraph.
package org.jmlspecs.samples.digraph;
import org.jmlspecs.models.JMLType;
/*@
@ public pure model class ArcType implements JMLType {
@
@ public model NodeType from;
@ public model NodeType to;
@ public invariant from != null && to != null;
@
@ public normal_behavior
@ requires from != null && to != null;
@ assignable this.from, this.to;
@ ensures this.from.equals(from) && this.to.equals(to);
@ public ArcType(NodeType from, NodeType to);
@
@ also
@ public normal_behavior
@ {|
@ requires o instanceof ArcType;
@ ensures \result <==> ((ArcType)o).from.equals(from)
@ && ((ArcType)o).to.equals(to);
@ also
@ requires !(o instanceof ArcType);
@ ensures \result == false;
@ |}
@ public boolean equals(Object o);
@
@ also
@ public normal_behavior
@ ensures \result instanceof ArcType
@ && ((ArcType)\result).equals(this);
@ public Object clone();
@ }
@*/
The use of also in the specification of
ArcType's equals method is interesting.
It separates two cases of the normal behavior for that method.
This is equivalent to using two public normal_behavior clauses,
one for each case.
That is, when the argument is an instance of ArcType,
the method must return true just when
this and o have the same from and to fields.
And when o is not an instance of ArcType,
the equals method must return false.
Finally, the specification of the class Digraph
is given in the file `Digraph.jml' shown below.
This specification
demonstrates how to use container classes,
like JMLValueSet, combined with
appropriate invariants to specify models that are compositions of
other classes.
Both the model fields nodes and arcs are of type
JMLValueSet. However, the first invariant clause restricts
nodes so that every object in nodes is, in fact, of type
NodeType.
Similarly, the next invariant clause we restrict arcs to be
a set of ArcType objects. In both cases, since the type is
JMLValueSet, membership is determined by
the equals method for the
type of the elements (rather than reference equality).
package org.jmlspecs.samples.digraph;
//@ model import org.jmlspecs.models.*;
public class Digraph {
//@ public model JMLValueSet nodes;
//@ public model JMLValueSet arcs;
/*@ public invariant nodes != null
@ && (\forall JMLType n; nodes.has(n); n instanceof NodeType);
@ public invariant arcs != null
@ && (\forall JMLType a; arcs.has(a); a instanceof ArcType);
@ public invariant (\forall ArcType a; arcs.has(a);
@ nodes.has(a.from) && nodes.has(a.to));
@*/
/*@ public normal_behavior
@ assignable nodes, arcs;
@ ensures nodes.isEmpty() && arcs.isEmpty();
@*/
public Digraph();
/*@ public normal_behavior
@ requires n != null;
@ assignable nodes;
@ ensures nodes.equals(\old(nodes.insert(n)));
@*/
public void addNode(NodeType n);
/*@ public normal_behavior
@ requires unconnected(n);
@ assignable nodes;
@ ensures nodes.equals(\old(nodes.remove(n)));
@*/
public void removeNode(NodeType n);
/*@ public normal_behavior
@ requires inFrom != null && inTo != null
@ && nodes.has(inFrom) && nodes.has(inTo);
@ assignable arcs;
@ ensures arcs.equals(
@ \old(arcs.insert(new ArcType(inFrom, inTo))));
@*/
public void addArc(NodeType inFrom, NodeType inTo);
/*@ public normal_behavior
@ requires inFrom != null && inTo != null
@ && nodes.has(inFrom) && nodes.has(inTo);
@ assignable arcs;
@ ensures arcs.equals(
@ \old(arcs.remove(new ArcType(inFrom, inTo))));
@*/
public void removeArc(NodeType inFrom, NodeType inTo);
/*@ public normal_behavior
@ assignable \nothing;
@ ensures \result == nodes.has(n);
@*/
public /*@ pure @*/ boolean isNode(NodeType n);
/*@ public normal_behavior
@ ensures \result == arcs.has(new ArcType(inFrom, inTo));
@
@*/
public /*@ pure @*/ boolean isArc(NodeType inFrom, NodeType inTo);
/*@ public normal_behavior
@ requires nodes.has(start) && nodes.has(end);
@ assignable \nothing;
@ ensures \result == reachSet(new JMLValueSet(start)).has(end);
@*/
public /*@ pure @*/ boolean isAPath(NodeType start, NodeType end);
/*@ public normal_behavior
@ assignable \nothing;
@ ensures \result <==>
@ !(\exists ArcType a; arcs.has(a);
@ a.from.equals(n) || a.to.equals(n));
@ public pure model boolean unconnected(NodeType n);
@*/
/*@ public normal_behavior
@ requires nodeSet != null
@ && (\forall JMLType o; nodeSet.has(o);
@ o instanceof NodeType && nodes.has(o));
@ {|
@ assignable \nothing;
@ also
@ requires nodeSet.equals(OneMoreStep(nodeSet));
@ ensures \result != null && \result.equals(nodeSet);
@ also
@ requires !nodeSet.equals(OneMoreStep(nodeSet));
@ ensures \result != null
@ && \result.equals(reachSet(OneMoreStep(nodeSet)));
@ |}
@ public pure model JMLValueSet reachSet(JMLValueSet nodeSet);
@*/
/*@ public normal_behavior
@ requires nodeSet != null
@ && (\forall JMLType o; nodeSet.has(o);
@ o instanceof NodeType && nodes.has(o));
@ assignable \nothing;
@ ensures \result != null
@ && \result.equals(nodeSet.union(
@ new JMLValueSet { NodeType n | nodes.has(n)
@ && (\exists ArcType a; a != null && arcs.has(a);
@ nodeSet.has(a.from) && n.equals(a.to))}));
@ public pure model JMLValueSet OneMoreStep(JMLValueSet nodeSet);
@*/
} // end of class Digraph
An interesting use of pure model methods appears at the end of
the specification of Digraph in the pure model method reachSet.
This method constructively defines the set of all nodes
that are reachable from the nodes in the argument nodeSet.
This specification uses a nested case analysis, between {|
and |}. The meaning of this is again that each pre- and postcondition
pair has to be obeyed, but by using nesting, one can avoid duplication of the
requires clause that is found at the beginning of the specification.
The measured_by clause is needed because this specification is
recursive; the measure given allows one to describe a termination argument,
and thus ensure that the specification is well-defined.
This clause defines an integer-valued measure that must always
be at least zero; furthermore, the measure for a call and recursive
uses in the specification must strictly decrease [Owre-etal95].
The recursion in the specification builds up the entire set
of reachable nodes by, for each recursive reference, adding the nodes
that can be reached directly (via a single arc) from the nodes in
nodeSet.
Following Dhara and Leavens [Dhara-Leavens96] [Leavens97c],
a subtype inherits the specifications of its supertype's
public and protected members (fields and methods),
as well as its public and protected
invariants and history constraints.(26)
This ensures that a subclass specifies a behavioral subtype of its
supertypes.
This inheritance can be thought of textually,
by copying the public and protected specifications
of the methods of a class's ancestors
and all interfaces that a class implements
into the class's specification and combining the specifications
using also [Raghavan-Leavens00].(27)
(This is the reason for the use of also at the beginning
of specifications in overriding methods.)
By the semantics of method combination using also,
these behaviors must all be satisfied by the method,
in addition to any explicitly specified behaviors.
For example, consider the class PlusAccount,
specified in file `PlusAccount.jml' shown below.
It is specified as a subclass of Account
(see section 2.4 Use of Pure Classes).
Thus it inherits the fields of Account,
and Account's public invariants, history constraints,
and method specifications.
(The specification of Account given above
does not have any protected specification information.)
Because it inherits the fields of its superclass,
inherited method specifications of behavior are still meaningful when copied
to the subclass.
The trick is to always add new model fields to the subclass and relate
them to the existing ones.
Note that in the represents clause below,
instead of a left-facing arrow, <-,
the connective "\such_that"
is used to introduce a relationship predicate.
This form of the represents clause allows one to specify abstraction relations,
instead of abstraction functions.
package org.jmlspecs.samples.prelimdesign;
public class PlusAccount extends Account {
//@ public model MoneyOps savings, checking; in credit;
/*@ public represents credit \such_that
@ credit.equals(savings.plus(checking));
@*/
//@ public invariant savings != null && checking != null;
/*@ public invariant_redundantly savings.plus(checking)
@ .greaterThanOrEqualTo(new USMoney(0));
@*/
/*@ public normal_behavior
@ requires sav != null && chk != null && own != null
@ && (new USMoney(1)).lessThanOrEqualTo(sav)
@ && (new USMoney(1)).lessThanOrEqualTo(chk);
@ assignable credit, owner;
@ assignable_redundantly savings, checking;
@ ensures savings.equals(sav) && checking.equals(chk)
@ && owner.equals(own);
@ ensures_redundantly credit.equals(sav.plus(chk));
@*/
public PlusAccount(MoneyOps sav, MoneyOps chk, String own);
/*@ also
@ public normal_behavior
@ requires 0.0 <= rate && rate <= 1.0
@ && credit.can_scaleBy(1.0 + rate);
@ assignable credit, savings, checking;
@ ensures checking.equals(\old(checking.scaleBy(1.0 + rate)));
@ for_example
@ public normal_example
@ requires rate == 0.05 && checking.equals(new USMoney(2000));
@ assignable credit, savings, checking;
@ ensures checking.equals(new USMoney(2100));
@*/
public void payInterest(double rate);
/*@ also
@ public normal_behavior
@ requires amt != null
@ && (new USMoney(0)).lessThanOrEqualTo(amt)
@ && amt.lessThanOrEqualTo(savings);
@ assignable credit, savings;
@ ensures savings.equals(\old(savings.minus(amt)))
@ && \not_modified(checking);
@ also
@ public normal_behavior
@ requires amt != null
@ && (new USMoney(0)).lessThanOrEqualTo(amt)
@ && amt.lessThanOrEqualTo(credit)
@ && amt.greaterThan(savings);
@ assignable credit, savings, checking;
@ ensures savings.equals(new USMoney(0))
@ && checking.equals(
@ \old(checking.minus(amt.minus(savings))));
@ for_example
@ public normal_example
@ requires savings.equals(new USMoney(40001))
@ && amt.equals(new USMoney(40000));
@ assignable credit, savings, checking;
@ ensures savings.equals(new USMoney(1))
@ && \not_modified(checking);
@ also
@ public normal_example
@ requires savings.equals(new USMoney(30001))
@ && checking.equals(new USMoney(10000))
@ && amt.equals(new USMoney(40000));
@ assignable credit, savings, checking;
@ ensures savings.equals(new USMoney(0))
@ && checking.equals(new USMoney(1));
@*/
public void withdraw(MoneyOps amt);
/*@ also
@ public normal_behavior
@ requires amt != null
@ && amt.greaterThanOrEqualTo(new USMoney(0))
@ && credit.can_add(amt);
@ assignable credit, savings;
@ ensures savings.equals(\old(savings.plus(amt)))
@ && \not_modified(checking);
@ for_example
@ public normal_example
@ requires savings.equals(new USMoney(20000))
@ && amt.equals(new USMoney(1));
@ assignable credit, savings, checking;
@ ensures savings.equals(new USMoney(20001));
@*/
public void deposit(MoneyOps amt);
/*@ public normal_behavior
@ requires amt != null
@ && amt.greaterThanOrEqualTo(new USMoney(0))
@ && credit.can_add(amt);
@ assignable credit, checking;
@ ensures checking.equals(\old(checking.plus(amt)))
@ && \not_modified(savings);
@ for_example
@ public normal_example
@ requires checking.equals(new USMoney(20000))
@ && amt.equals(new USMoney(1));
@ assignable credit, checking;
@ ensures checking.equals(new USMoney(20001));
@*/
public void depositToChecking(MoneyOps amt);
/*@ public normal_behavior
@ requires amt != null;
@ {|
@ requires (new USMoney(0)).lessThanOrEqualTo(amt)
@ && amt.lessThanOrEqualTo(checking);
@ assignable credit, checking;
@ ensures checking.equals(\old(checking.minus(amt)))
@ && \not_modified(savings);
@ also
@ requires (new USMoney(0)).lessThanOrEqualTo(amt)
@ && amt.lessThanOrEqualTo(credit)
@ && amt.greaterThan(checking);
@ assignable credit, checking, savings;
@ ensures checking.equals(new USMoney(0))
@ && savings.equals(
@ \old(savings.minus(amt.minus(checking))));
@ |}
@ for_example
@ public normal_example
@ requires checking.equals(new USMoney(40001))
@ && amt.equals(new USMoney(40000));
@ assignable credit, checking;
@ ensures checking.equals(new USMoney(1))
@ && \not_modified(savings);
@ also
@ public normal_example
@ requires savings.equals(new USMoney(30001))
@ && checking.equals(new USMoney(10000))
@ && amt.equals(new USMoney(40000));
@ assignable credit, checking, savings;
@ ensures checking.equals(new USMoney(0))
@ && savings.equals(new USMoney(1));
@*/
public void payCheck(MoneyOps amt);
}
Go to the first, previous, next, last section, table of contents.