| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
In this section we give some examples of JML class specifications that illustrate the basic features of JML.
2.1 Abstract Models 2.2 Data Groups 2.3 Types For Modeling 2.4 Use of Pure Classes 2.5 Composition for Container Classes 2.6 Behavioral Subtyping
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.
2.1.1 Model Fields 2.1.2 Invariants 2.1.3 Method Specifications 2.1.4 Models and Lightweight Specifications
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 is not part of the Java implementation, and must appear
in an annotation;
however, for purposes of the specification we treat it 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 is not part of
the Java implementation, since it is modified by the keyword
model.
Such model imports must also appear in annotation comments.
In general, any declaration form in Java can have the model 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 be true
of the field's starting value.
That is,
all reachable objects of the type UnboundedStack
must 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.(9)
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.
2.1.3.1 The Assignable Clause 2.1.3.2 Old Values 2.1.3.3 Reference Semantics 2.1.3.4 Correct Implementation
The use of the assignable(10) 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),
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,(11) 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.(12) 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 the locations corresponding to formal
parameters in the assignable clause.
However, the locations corresponding to fields or array elements of
such formal parameters can be sensibly mentioned 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 to 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 must use equals instead of == to compare
instances of this type for equality of values. For example, in
the postcondition of the pop method, we use equals
to compare theStack and \old(theStack.trailer()),
as these may yield different objects.
Using == would be a mistake, since it would only compare them
for object identity.
As in Java itself, most types are reference types, and hence many expressions
yield references (i.e., object identities or addresses),
as opposed to primitive values.
This means that ==, except when used to compare
pure values of primitive types such as boolean or int,
is reference equality.
As in Java,
to get value equality for reference types one uses the
equals method in assertions.
For example, the predicate
myString == yourString, is only true if
the objects denoted by myString and yourString are the
same object (i.e., if the names are aliases);
to compare their values one must write
myString.equals(yourString).
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.
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);
//@ public invariant !Double.isNaN(y);
//@ public invariant !Double.isInfinite(x);
//@ public invariant !Double.isInfinite(y);
//@ ensures x == 0.0 && y == 0.0;
public Point2D() { }
/*@ requires !Double.isNaN(xc);
@ requires !Double.isNaN(yc);
@ requires !Double.isInfinite(xc);
@ requires !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 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 without
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.
2.2.1 Specification of BoundedThing 2.2.2 Specification of BoundedStackInterface
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_only CloneNotSupportedException;
@*/
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.(13)
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,(14)
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-Leavens05].
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-Leavens05].
ensures false; |
This formalizes the idea that a method with an exceptional_behavior
specification may not return normally
when the specification's precondition is satisfied.
Thus, when the precondition of 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 the
signals_only clause.
The signals_only clause in the example says that the method may
only throw an exception that is a subtype of
CloneNotSupportedException when the exceptional behavior's
precondition is true. This says the same thing as the following,
more verbose, signals clause.
signals (Exception e) e instanceof CloneNotSupportedException; |
The signals clause itself 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, a signals clause of the
form
signals (CloneNotSupportedException) true; |
would only say that a CloneNotSupportedException can always be thrown;
it would not prohibit other exceptions
that are not subtypes of CloneNotSupportedException from being
thrown.
For example, if clone were specified with such a signals
clause, then an implementation could legally throw a
NullPointerException. To prevent such a possibility, in many
cases it is preferable to use a signals_only clause to limit
what exceptions may be thrown.
Finally note that in the specification of clone,
the normal 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_only 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_only BoundedStackException, NullPointerException;
@ 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_only BoundedStackException;
@ signals (BoundedStackException e)
@ \fresh(e) && e != null && e.getMessage() != null
@ && e.getMessage().equals("empty stack");
@*/
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.
2.2.2.1 Data Groups and Represents Clauses 2.2.2.2 Redundant Specification 2.2.2.3 Multiple Specification Cases 2.2.2.4 Pitfalls in Specifying Exceptions 2.2.2.5 Redundant Ensures Clauses
The in and represents clauses
that follow the declaration of theStack
are an important feature in modeling
with layers of model fields.(15)
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.(16)
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.
After 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-Leavens05] 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 default signals clause has been added.
This clause was omitted from the original specification, since no
particular details of the exception object were important to the specifier.
//@ 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_only BoundedStackException;
@ signals (java.lang.Exception) 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.
To compensate for this, the predicate \not_assigned, is used in
the exceptional behavior specification cases to prohibit assignment to
the locations (those in the data groups of size and theStack)
that are now part of the assignable clause.
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_only BoundedStackException;
@ signals (java.lang.Exception)
@ \old(!theStack.isEmpty()) ==> false;
@ signals (java.lang.Exception)
@ \old(theStack.isEmpty()) ==>
@ \not_assigned(size) && \not_assigned(theStack)
@ && 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 simultaneously, 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.(17)
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 multiple signals_only clauses or
using multiple signals clauses like:
signals (Exception e) e instanceof BoundedStackException; |
BoundedStackException to be thrown when the
precondition is true, one can write a signals clause like:
signals (BoundedStackException); |
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.(18)
In summary, using types like JMLObjectSequence for modeling can
help the specifier give more precise specifications. We describe more
about such types in the next section.
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.
2.3.1 Purity 2.3.2 Money 2.3.3 MoneyComparable and MoneyOps 2.3.4 MoneyAC 2.3.5 MoneyComparableAC 2.3.6 USMoney
We say a method
is pure if it is either specified with
the modifier pure or is a 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 has the clauses
diverges false;
assignable \nothing;
|
A pure constructor has the clauses
diverges false;
assignable this.*;
|
Implementations of pure methods and constructors
will be checked to see that they meet these conditions; i.e., that
pure methods do not assign to locations that exist in the pre-state, and
that pure constructors only assign to pre-existing locations that
are fields of the this object.
To make such checking modular, some JML tools prohibit a pure method
or constructor implementation from calling methods or constructors
that are not pure. However, more sophisticated tools could more
directly check the intended semantics [Salcianu-Rinard05].
A pure method or constructor must also be provably terminating. Although JML does not force users to make such proofs of termination, users writing pure methods and constructors are supposed to make pure methods total in the sense that whenever, a pure method is called it either returns normally or throws some exception. This is supposed to lessen the possibility that assertion evaluation could loop forever, help make pure methods more like mathematical functions, and help the runtime assertion checker. The runtime assertion checker turns exceptions into arbitrary values of the appropriate result type [Cheon03] [Cheon-Leavens05]; it cannot do anything with infinite loops.
Furthermore, a pure method is supposed to always either terminate normally or throw an exception, even for calls that do not satisfy its precondition. Static verification tools for JML should enforce this condition, by requiring a proof that a pure method implementation satisfies the following specification
private behavior
requires true;
diverges false;
assignable \nothing;
|
assignable this.*; for constructors).
However, this implicit verification condition is a specification, and is thus cannot be used in reasoning about calls to the method, even calls from within the class itself and recursive calls from within the implementation. For this reason we recommend writing the method or constructor specification in such a way that the effective precondition of the method is "true," making the proof of the above implicit verification condition trivial, and allowing the termination behavior of the implementation to be relied upon by all clients.
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.
Furthermore, a pure method must be deterministic, in the sense that when called in a given state, it must always return the same value. Similarly a pure constructor should be deterministic in the sense that when called in a given state, it always initializes the object in the same way.
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.
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);
conversely, a Java method can be pure (and thus 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(/*@ nullable @*/ 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.(19)
The following explain more aspects of JML related to the above specification.
2.3.2.1 Redundant Examples 2.3.2.2 JMLType and Informal Predicates
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(20)
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()),
\old()),
and
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.20 $
* @author Gary T. Leavens and 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(/*@ nullable @*/ 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.(21)
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.
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
@ old boolean can_add = can_add(m2); // FIXME: inline.
@ requires m2 != null && can_add;
@ 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
@ old boolean inRange = inRange((double) pennies - m2.pennies); // FIXME: inline.
@ requires m2 != null
@ && inRange;
@ 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.(22)
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(/*@ nullable @*/ 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.(23)
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)
{
return new USMoney(numCents + totalCents(m2));
}
public MoneyOps minus(Money m2)
{
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 clause 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
@ old boolean can_scale = credit.can_scaleBy(1.0 + rate);
@ requires 0.0 <= rate && rate <= 1.0
@ && can_scale;
@ 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
@ old boolean can_add = credit.can_add(amt);
@ requires amt != null
@ && amt.greaterThanOrEqualTo(new USMoney(0))
@ && can_add;
@ 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 and the postcondition
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.
2.5.1 NodeType 2.5.2 ArcType 2.5.3 Digraph
The file `NodeType.java'
contains the specification of an interface NodeType.
We also declare this interface to be pure,
since we want to use its methods in the specifications of other
classes.
(This is appropriate, since all the methods of NodeType are
side-effect free.)
package org.jmlspecs.samples.digraph;
import org.jmlspecs.models.*;
public /*@ pure @*/ interface NodeType extends JMLType {
/*@ also
@ public normal_behavior
@ requires !(o instanceof NodeType);
@ ensures \result == false;
@*/
public boolean equals(/*@ nullable @*/ Object o);
public int hashCode();
/*@ also
@ public normal_behavior
@ ensures \result instanceof NodeType
@ && ((NodeType)\result).equals(this);
@*/
public Object clone();
}
|
ArcType is specified as a
pure class in the file `ArcType.jml' shown below.
In theory, this class could have been declared with the model modifier,
since it does not appear in the interface
to Digraph. However, we specify it as a normal Java class for
simplicity, and because model classes do not currently work in JML's
runtime assertion checker.
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;
/*@ pure @*/ public 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(/*@ nullable @*/ 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.
In this specification, the container class JMLValueSet is used
as the type of the model fields nodes and arcs.
Since JML currently only works with a non-generic version of Java,
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_redundantly nodes != null;
@ public invariant (\forall JMLType n; nodes.has(n);
@ n instanceof NodeType);
@ public invariant_redundantly arcs != null;
@ public invariant (\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_redundantly 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_redundantly inFrom != null && inTo != null;
@ requires 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_redundantly inFrom != null && inTo != null;
@ requires 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
@ requires_redundantly inFrom != null && inTo != null;
@ 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 @*/ boolean unconnected(NodeType n);
/*@ public normal_behavior
@ requires_redundantly nodeSet != null;
@ requires (\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_redundantly nodeSet != null;
@ requires (\forall JMLType o; nodeSet.has(o);
@ o instanceof NodeType && nodes.has(o));
@ assignable \nothing;
@ ensures_redundantly \result != null;
@ ensures \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);
@*/
}
|
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.
As in Java, a subtype inherits members (fields and methods) from its supertypes. A subtype also inherits all the class level-specifications associated with fields and all method specifications for public and protected instance methods. This specification inheritance has the effect of making the subtype a behavioral subtype [Liskov-Wing94], in the sense that instances of the subtype obey the specifications its supertype(s) [Dhara-Leavens96] [Leavens-Weihl95].
Class-level specifications associated with fields include include
invariants and history constraints (see section 2.2.1.2 Invariants and History Constraint),
as well as initially clauses (see section 2.1.1 Model Fields)
data group declarations (see section 2.2 Data Groups),
and represents clauses (see section 2.2.2.1 Data Groups and Represents Clauses).
Inheritance of invariants means that
each supertype's invariants must also hold in the subtype.
Similarly, every history constraint specified in each supertype must
be obeyed in the subtype. And all initially clauses specified
for supertype fields must also be obeyed in all subtypes.
Fields declared in a supertype retain their data group
membership when inherited. Their represents clauses are also
inherited.
As in Java, private fields are inherited by a subtype but not visible to it. Similarly, default privacy (i.e., package visibility) fields are not accessible if the subtype is declared in a different package than the supertype declaring the field. As in Java, these fields are present in the objects of the subtype, but not accessible to code written in the subtype. In the same way, class level specifications associated with such fields must still be obeyed by objects of the subtype. Various restrictions to JML that ensure that this is always possible are being investigated [Ruby-Leavens00].
Specifications for instance methods are also inherited in the sense that public and protected specification cases must be obeyed by all overriding methods [Dhara-Leavens96] [Leavens97c]. This inheritance of method specifications ensures that a client's reasoning about a method call will still be valid, even if the method is overridden [America87] [America91] [Leavens-Weihl95], and thus that a subclass is a behavioral subtype of its supertypes [Dhara-Leavens96]. Note that private and default (package) visibility specification cases are not visible to subtypes, and hence do not have to be obeyed by them; not inheriting such specification cases does not cause clients reasoning problems, as these specification cases are not visible to clients making method calls (in general).(24) Furthermore, specifications are not inherited for constructors or for static methods, since they are not involved in dynamic dispatch.
Inheritance of method specifications can be thought of textually.
For each instance method, m specified in a class C,
one can imagine copying into the specification of m the public and protected
specification cases for m given in all of C's ancestors
and in all the interfaces C implements;
these specification cases would be combined using
also [Dhara-Leavens96] [Raghavan-Leavens05].(25)
(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.)
Since it inherits the fields of its superclass,
a textual copy of the method specification cases of Account
would still be meaningful in the context of PlusAccount.
Thinking of such textual copies works if one adds new (model) fields to
specify the subclass and relates them to the existing ones.
If instead one tried to respecify the fields of a supertype
with invariants and history constraints
that violated the (inherited) specification of that supertype, then
the resulting specification would be contradictory, and hence not be
correctly implementable.
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
@ old boolean can_scale = credit.can_scaleBy(1.0 + rate);
@ requires 0.0 <= rate && rate <= 1.0
@ && can_scale;
@ 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
@ old boolean can_add = credit.can_add(amt);
@ requires amt != null
@ && amt.greaterThanOrEqualTo(new USMoney(0))
@ && can_add;
@ 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
@ old boolean can_add = credit.can_add(amt);
@ requires amt != null
@ && amt.greaterThanOrEqualTo(new USMoney(0))
@ && can_add;
@ 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);
}
|
Similarly, if one tried to respecify a method in a way that violated an (inherited) specification case, then the method would have to obey both specifications, and would not be correctly implementable. Thus, specification inheritance guarantees that all subtypes are behavioral subtypes in JML, and trying to avoid behavioral subtyping results in unimplementable specifications Dhara-Leavens96.
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.
| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |