| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
JML is a behavioral interface specification language tailored to Java. It is designed to be written and read by working software engineers, and should require only modest mathematical training. It uses Eiffel-style syntax combined with model-based semantics, as in VDM and Larch. JML supports quantifiers, specification-only variables, and other enhancements that make it more expressive for specification than Eiffel and easier to use than VDM and Larch.
JML [Leavens-Baker-Ruby01], which stands for "Java Modeling Language," is a behavioral interface specification language (BISL) [Wing87] designed to specify Java [Arnold-Gosling98] [Gosling-Joy-Steele96] modules. Java modules are classes and interfaces.
A behavioral interface specification describes both the details of a module's interface with clients, and its behavior from the client's point of view. Such specifications are not good for the specification of whole programs, but are good for recording detailed design decisions or documentation of intended behavior, for a software module.
The goal of this chapter is to explain JML and the concepts behind its approach to specification. Since JML is used in detailed design of Java modules, we use the detailed design of an interface and class for priority queues as an example. The rest of this section explains interfaces and behavioral interface specification. In the next section we describe how to specify new types as conceptual models for detailed design. Following that we finish the example by giving the details of a class specification. We conclude after mentioning some other features of JML.
1.1 Interfaces 1.2 A First Example of Behavioral Specification
A module's interface consists of its name, and the names and types of its fields and methods. Java interfaces declare such interface information, but class declarations do as well. As in the Larch family of BISLs [Guttag-Horning93] [LeavensLarchFAQ] [Wing87] [Wing90a], interface information in JML is declared using the declaration syntax of the programming language to which the BISL is tailored; thus, JML uses Java declaration syntax.
An example is given in the file
`PriorityQueueUser.java-refined', which is shown below.
This example gives the information a Java program needs
to use a PriorityQueueUser object,
including the package to which it belongs, the accessibility of the
methods (public), the names of the methods,
the types of their arguments and results, and what
exceptions they can throw.
package org.jmlspecs.samples.jmlkluwer;
public interface PriorityQueueUser {
/*@ pure @*/ boolean contains(Object argObj);
/*@ pure @*/ Object next() throws PQException;
void remove(Object argObj);
/*@ pure @*/ boolean isEmpty();
}
|
Also included in the above file are three JML annotations.
These annotations are enclosed within these annotation comments
of the form /*@ ... @*/;
one can also write annotation comments using the form //@,
and such comments extend to the end of the corresponding line.(1)
Java ignores both kinds of JML annotation comments,
but they are significant to JML.
The pure annotations on the methods next,
contains, and isEmpty require these methods to be
pure, meaning that they cannot have any side effects.
In JML, behavioral specification information is also given in the form
of annotations.
As in the Larch approach, such specifications are model-based.
That is, they are stated in terms of a mathematical model
[Guttag-Horning93] [Hoare72a] [Wing83] [Wing87]
of the states (or values) of objects.
Unlike most Larch-style specification languages, however,
in JML such models are described by declaring model fields,
which are only used for purposes of specification.
In JML, a declaration can include the modifier model,
which means that the declaration need not appear in a correct implementation;
all non-model declarations must appear in a correct implementation.
As an example, the file `PriorityQueueUser.jml-refined' below
specifies a model for priority queues.
This specification is a refinement of the one
given in the file (shown above) `PriorityQueueUser.java-refined',
which is why the refine clause appears in the specification
following the package declaration.
The meaning of the refine clause is that the given specification adds
to the one in the file named, by imposing additional constraints
on that specification.
Such a refinement might be done,
for example, when one is starting to make detailed design decisions
or when starting to specify the behavior of existing software modules.
In a refinement, existing specification information is inherited;
that is, the method declarations in the interface PriorityQueueUser
are inherited, and thus not
repeated below.
package org.jmlspecs.samples.jmlkluwer;
//@ refine "PriorityQueueUser.java-refined";
//@ model import org.jmlspecs.models.*;
public interface PriorityQueueUser {
/*@ public model instance JMLValueSet entries;
@ public initially entries.isEmpty();
@*/
/*@ public instance invariant
@ (\forall JMLType e; entries.has(e);
@ e instanceof QueueEntry);
@ public instance invariant
@ (\forall QueueEntry e1; entries.has(e1);
@ (\forall QueueEntry e2;
@ entries.has(e2) && !(e1.equals(e2));
@ e2.obj != e1.obj
@ && e2.timeStamp != e1.timeStamp ) );
@*/
}
|
Following the refine clause above is a model import declaration.
This has the effect like a Java import declaration for JML,
but the use of model means
that the import does not have to appear
in an implementation, as it is only needed for specification purposes.
The package being imported, org.jmlspecs.models,
consists of several pure classes including sets, sequences, relations,
maps, and so on, which are useful in behavioral specification.
These fill the role of the built-in types used for specification in VDM and Z,
or the traits used in Larch.
Since they are pure (side-effect free) classes,
they can be used in assertions without affecting the state of
the computation, which allows assertions to have a well-defined
mathematical meaning (unlike Eiffel's assertions).
However, since they are Java classes, their methods are invoked using
the usual Java syntax.
In the specification above we use the class JMLValueSet
as the type of the model field entries.
That is, for purposes of specification, we imagine that every
object that implements the interface PriorityQueueUser
has a public field entries of type JMLValueSet.
This model field appears (to clients) to have started out initially
as empty, as stated in the initially clause
attached to its declaration
[Ogden-etal94] [Morgan94].
The two invariant clauses further describe the intended state
of entries.
The first states that all of its elements
have type QueueEntry.
(By default JML implicitly adds an invariant that entries
is non-null [Chalin-Rioux05].)
The \forall notation is an addition to the Java syntax for
expressions; it gives universal quantification over the declared variables.
Within such an expression of the form (\forall T x; R(x); P(x)),
the expression R(x) specifies the range over which the bound
variable, x, can take on values; it is separated from the
term predicate, P(x), by a semicolon (;).
For example, the first invariant means that for all
JMLType objects e such that entries.has(e),
e has type QueueEntry.
The second invariant states that every such QueueEntry object
has a unique obj and timeStamp.
In the file `PriorityQueueUser.java' below
we make yet another refinement,
to specify the behavior of the methods of PriorityQueueUser.
This specification, because it refines the
specification in `PriorityQueueUser.jml-refined',
inherits the model fields specified there, as well as the initially
and invariant clauses.
(Inheritance of specifications is explained further below.)
package org.jmlspecs.samples.jmlkluwer;
//@ refine "PriorityQueueUser.jml-refined";
public interface PriorityQueueUser {
/*@ also
@ public normal_behavior
@ ensures \result <==>
@ (\exists QueueEntry e; entries.has(e);
@ e.obj == argObj);
@*/
/*@ pure @*/ boolean contains(Object argObj);
/*@ also
@ public normal_behavior
@ requires !entries.isEmpty();
@ ensures
@ (\exists QueueEntry r;
@ entries.has(r) && \result == r.obj;
@ (\forall QueueEntry o;
@ entries.has(o) && !(r.equals(o));
@ r.priorityLevel >= o.priorityLevel
@ && (r.priorityLevel == o.priorityLevel
@ ==> r.timeStamp < o.timeStamp) ) );
@ also
@ public exceptional_behavior
@ requires entries.isEmpty();
@ signals_only PQException;
@*/
/*@ pure @*/ Object next() throws PQException;
/*@ also
@ public normal_behavior
@ requires contains(argObj);
@ assignable entries;
@ ensures (\exists QueueEntry e;
@ \old(entries.has(e)) && e.obj == argObj;
@ entries.equals(\old(entries.remove(e))));
@ also
@ public normal_behavior
@ requires !contains(argObj);
@ assignable \nothing;
@ ensures \not_modified(entries);
@*/
void remove(Object argObj);
/*@ also
@ public normal_behavior
@ ensures \result <==> entries.isEmpty();
@*/
/*@ pure @*/ boolean isEmpty();
}
|
The specification of contains above shows the simplest form of a
behavioral specification for a method:
a single public normal_behavior clause
followed by a method header.
This specification says that the method
returns true just when its argument is the same as some object in the queue.
The public normal_behavior clause in this specification
consists of a single ensures clause.
This ensures clause gives the method's total-correctness
postcondition;
that is, calls to contains must terminate
(as opposed to looping forever or aborting)
in a state that satisfies the postcondition.
The public keyword says that the specification is intended for clients;
while the "normal" in normal_behavior prohibits throwing exceptions.
The meaning of && and == are as in Java;
that is, && is short-circuit logical conjunction,
and e.obj == argObj means that e.obj and argObj
are the same object.
The keyword \result denotes the return value of the method,
which in this case is a boolean.
The operator <==> means "if and only if";
it is equivalent to == for booleans, but has a lower precedence.
The notation \exists is used for existential quantification.
Like universal quantifiers,
existential quantifiers can also have a range expression
that is separated from the term expression by a semicolon (;).
The specification of the method next shows one way to specify
methods with exceptions in JML.
This uses a public normal_behavior clause for the case where no
exceptions are thrown, and an public exceptional_behavior
clause for when exceptions are thrown.
The semantics is that a correct implementation must satisfy
both of these behaviors [Leavens-Baker99] [Wills94] [Wing83].
In the specification of next,
the public exceptional_behavior clause states that
only an instance of the PQException class
(not shown here) may be thrown when entries is empty.
The requires clause gives a precondition for that case,
and when it is true, the method must terminate
(in this case by throwing an exception).
Since no other exceptions are allowed, this effectively says that the
method must thorw an instance of PQException when the
exceptional behavior's precondition is satisfied by a call.
as that case's postcondition must be satisfied.
The public normal behavior of next must be obeyed
when its precondition is true;
that is, when entries is not empty.
The normal behavior's postcondition
says that next returns an object with the lowest timestamp
in the highest priority level.
It would, of course, be possible to only specify the public normal behavior
for next. If this were done,
then implementations could just assume the precondition of
the normal behavior--that entries is not empty.
That would be an appropriate design for clients that can be trusted,
and might permit more efficient implementation.
The given specification is appropriate for untrusted clients
[Meyer92a] [Meyer97].
The specification remove uses case analysis
[Leavens-Baker99] [Wills94] [Wing83]
in the specification of normal behavior.
The two cases are separated by the keyword also,
and each must be obeyed when its precondition is true.
The first case contains a assignable clause.(2)
This is a frame condition
[Borgida-Mylopoulos-Reiter95];
it states that only the fields mentioned
(and any on which they depend [Leino95] [Leino95a])
can be assigned to; no other fields, including fields in other objects,
can be assigned.
Omitting the assignable clause means that all fields
can be assigned.
(Technically, the assignable clause is also concerned with array elements.
Local variables, including the formal parameters of a method,
and also fields of newly-created objects may also be
freely assigned by a method [Leavens-Baker-Ruby01].)
Note that the precondition of remove uses the method contains,
which is permitted because it is pure.
The most interesting thing about the specification of remove
is that it uses the JML reserved word \old.
As in Eiffel,
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.
While we have broken up the specification of PriorityQueueUser
into three pieces, that was done partly to demonstrate refinement and partly
so that each piece would fit on a page.
In common use, this specification would be written in one file.
| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |