| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This chapter discusses JML's model programs, which are adapted from the refinement calculus [Back88] [Back-vonWright89a] [Buechi-Weck00] [Morgan94] [Morris87]. Details of JML's design and semantics for model program specifications are described in a recent paper [Shaner-Leavens-Naumann07].
The basic idea of a model program is that it is a specification that is written as an abstract algorithm. Such an abstract algorithm specifies a method in the sense that the method's execution should be a refinement of the model program.
JML adopts ideas from B@"{u}chi and Weck's "grey-box approach" to specification [Buechi-Weck00] [Buechi00]. However, JML structurally restricts the notion of refinement by not permitting all implementations with behavior that refines the model program, but only allowing implementations that syntactically match the model program [Shaner-Leavens-Naumann07]. The current JML notion of matching uses refining-statements (see section 13.4.3 Refining Statements), as explained below. This turns out to be a simple and easy to understand technique for specifying and verifying both higher-order features and callbacks.
Consider the following example (from a survey on behavioral subtyping by Leavens and Dhara [Leavens-Dhara00]). In this example, both the methods are specified using model programs, which are explained below.
package org.jmlspecs.samples.dirobserver;
//@ model import org.jmlspecs.models.JMLString;
//@ model import org.jmlspecs.models.JMLObjectSetEnumerator;
/** Directories that can be both read and written. */
public interface Directory extends RODirectory {
/** Add a mapping from the given string
* to the given file to this directory.
*/
/*@ public model_program {
@ normal_behavior
@ requires !in_notifier && n != null && n != "" && f != null;
@ assignable entries;
@ ensures entries != null
@ && entries.equals(\old(entries.extend(
@ new JMLString(n), f)));
@
@ maintaining !in_notifier && n != null && n != "" && f != null
@ && e != null;
@ decreasing e.uniteratedElems.size();
@ for (JMLObjectSetEnumerator e = listeners.elements();
@ e.hasMoreElements(); ) {
@ set in_notifier = true;
@ ((DirObserver)e.nextElement()).addNotification(this, n);
@ set in_notifier = false;
@ }
@ }
@*/
public void addEntry(String n, File f);
/** Remove the entry with the given name from this directory. */
/*@ public model_program {
@ normal_behavior
@ requires !in_notifier && n != null && n != "";
@ assignable entries;
@ ensures entries != null
@ && entries.equals
@ (\old(entries.removeDomainElement(
@ new JMLString(n))));
@
@ maintaining !in_notifier && n != null && n != "" && e != null;
@ decreasing e.uniteratedElems.size();
@ for (JMLObjectSetEnumerator e = listeners.elements();
@ e.hasMoreElements(); ) {
@ set in_notifier = true;
@ ((DirObserver)e.nextElement()).removeNotification(this, n);
@ set in_notifier = false;
@ }
@ }
@*/
public void removeEntry(String n);
}
|
Both model programs in the above example are formed from a specification
statement, which begins with the keyword normal_behavior in these
examples, and a for-loop. The key event in the for loop bodies is a
method call to a method (addNotification
or removeNotification). These calls must occur in a state
equivalent to the one reached in the model program for the
implementation to be legal.
The specification statements abstract away part of a correct implementation.
The normal_behavior statements in these examples both have a
precondition, a frame axiom, and a postcondition. These mean that the
statements that they abstract away from must be able to, in any state
satisfying the precondition, finish in a state satisfying the
postcondition, while only assigning to the locations (and their
dependees) named in the frame axiom.
For example, the first specification statement says that whenever
in_notifier is false, n is not null and not empty, and
f is not null, then this part of the method can assign to
entries something that isn't null and that is equal to the old
value of entries extended with a pair consisting of the string
n and the file f.
The model field entries, of type JMLValueToObjectMap,
is declared in the supertype RODirectory [Leavens-Dhara00].
Implementations of model programs must match each specification statement in a model program with a corresponding refining statement. In the matching refining statement, the specification part must be textually equal to the specification statement. The body of the refining statement must thus implement the given specification for that statement (see section 13.4.3 Refining Statements).
Since refining statements contain both specifications and
implementations, it is possible to extract a model program
specification from an implementation with (zero or more) refining
statements. This is done by using the modifier extract on the
method [Shaner-Leavens-Naumann07].
[[[Give example.]]]
The following gives the syntax of model programs. See section 13. Statements and Annotation Statements, for the parts of the syntax of statements that are unchanged from Java. The jml-compound-statement and jml-statement syntax is the same as the compound-statement and statement syntax, except that model-prog-statements are not flagged as errors within the jml-compound-statement and jml-statements.
model-program ::= [ privacy ] [ |
The syntax of the nondeterministic-choice statement is as follows.
nondeterministic-choice ::= |
The meaning is that a correct implementation can dynamically execute
(e.g., with an if or switch statement), one of the alternatives.
Code may also make a static choice of one of the alternatives.
nondeterministic-if ::= |
The meaning of a nondeterministic if statement is that a correct
implementation may dynamically choose any of the guarded-statements
for which the guard (the first assume-statement in the
guarded-statement) is true. If none of these are true, then it
must execute the jml-compound-statement given following
else, but it may not do that if one of the guards in the
guarded statements is true.
The grammar for specification statements appears below. It is
unusual, compared to specification statements in refinement calculus,
in that it allows one to specify statements that can signal
exceptions, or terminate abruptly. The reasons for this are based on
verification logics for Java [Huisman01] [Jacobs-Poll01] [Ruby06], which have
these possibilities. The meaning of an abrupt-spec-case is that
the normal termination and signaling an exception are forbidden; that
is, the equivalent spec-statement using behavior would
have ensures false; and signals (Exception) false;
clauses. Hence in an abrupt-spec-case, JML does not allow use
of an ensures-clause, signals-only-clause, or
signals-clause.
spec-statement ::= [ privacy ] behavior-keyword
generic-spec-statement-case
| [ privacy ] exceptional-behavior-keyword
exceptional-spec-case
| [ privacy ] normal-behavior-keyword
normal-spec-case
| [ privacy ] abrupt-behavior-keyword
abrupt-spec-case
generic-spec-statement-case ::= [ spec-var-decls ]
generic-spec-statement-body
| [ spec-var-decls ]
spec-header
[ generic-spec-statement-body ]
generic-spec-statement-body ::= simple-spec-statement-body
| |
The meaning of a spec-statement is that the code in a correct implementation must refine the given specification. One way to ensure this is to use a refining-statement in the implementation that contains the spec-statement in its specification part (see section 13.4.3 Refining Statements).
The following subsections describe details of each of the new clauses that may appear in an abrupt-spec-case or a generic-spec-statement-case.
15.6.1 Continues Clause 15.6.2 Breaks Clause 15.6.3 Returns Clause
continues-clause ::= continues-keyword [ target-label ]
[ pred-or-not ] |
The meaning of the continues-clause is that if the statement that
implements the specification statement executes a continue,
then it must continue to the given target-label (if any),
and the given predicate (if any) must hold in the state just before
the continue is executed.
A continues-clause should only be used in a
generic-spec-statement-case (with the keyword behavior)
or an abrupt-spec-case (with the keyword abrupt_behavior),
as in other kinds of
specification cases the default pred-or-not is false.
(See section 9.6.1 Semantics of flat behavior specification cases, for the
defaults for a lightweight and heavyweight specification cases.)
breaks-clause ::= breaks-keyword [ target-label ]
[ pred-or-not ] |
The meaning of the breaks-clause is that if the statement that
implements the specification statement executes a break,
then it must break to the given target-label (if any),
and the given predicate (if any) must hold in the state just before
the break is executed.
A breaks-clause should only be used in a
generic-spec-statement-case (with the keyword behavior)
or an abrupt-spec-case (with the keyword abrupt_behavior),
as in other kinds of
specification cases the default pred-or-not is false.
(See section 9.6.1 Semantics of flat behavior specification cases, for the
defaults for a lightweight and heavyweight specification cases.)
returns-clause ::= returns-keyword [ pred-or-not ] |
The meaning of the returns-clause is that if the statement that
implements the specification statement executes a return,
then the given predicate (if any) must hold in the state following
evaluation of the return value, but just before
the return is executed.
The predicate (if any) in a returns clause may use \result
to name the computed return value.
A returns-clause should only be used in a
generic-spec-statement-case (with the keyword behavior)
or an abrupt-spec-case (with the keyword abrupt_behavior),
as in other kinds of
specification cases the default pred-or-not is false.
(See section 9.6.1 Semantics of flat behavior specification cases, for the
defaults for a lightweight and heavyweight specification cases.)
| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |