| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This chapter describes the way JML can be used to specify abstract data types (ADTs).
Overall the mechanisms used in JML to specify ADTs can be described as follows. First, the interface of a type is described using the Java syntax for such a type's declaration (see section 7. Class and Interface Member Declarations); this includes any required fields and methods, along with their types and visibilities, etc. Second, the behavior of a type is described by declaring model and ghost fields to be the client (or subtype) visible abstractions of the concrete state of the objects of that type, by writing method specifications using those fields, and by writing various jml-declarations to further refine the logical model defined by these fields. These jml-declarations can also be used to record various design and implementation decisions.
The syntax of these jml-declarations is as follows.
jml-declaration ::= modifiers invariant
| modifiers history-constraint
| modifiers represents-clause
| modifiers initially-clause
| modifiers monitors-for-clause
| modifiers readable-if-clause
| modifiers writable-if-clause
| axiom-clause
|
The semantics of each of kind of jml-declaration is discussed in the sections below. However, before getting to the details, we start with some introductory examples.
[[[Need examples here, which should be first written into the org.jmlspecs.samples.jmlrefman package and then included and discussed here.]]]
The syntax of an invariant declaration is as follows.
invariant ::= invariant-keyword predicate |
An example of an invariant is given below.
The invariant in the example has default (package) visibility,
and says that in every state that is a visible state for an object of
type Invariant, the object's field b
is not null and the array it refers to has exactly 6 elements.
In this example, no postcondition is necessary for the constructor
since the invariant is an implicit postcondition for it.
package org.jmlspecs.samples.jmlrefman;
public abstract class Invariant {
boolean[] b;
//@ invariant b != null && b.length == 6;
//@ assignable b;
Invariant() {
b = new boolean[6];
}
}
|
Invariants are properties that have to hold in all visible states. The notion of visible state is of crucial importance in the explanation of the semantics of both invariants and constraints. A state is a visible state for an object o if it is the state that occurs at one of these moments in a program's execution:
Note that visible states for an object o do not include states at
the beginning and end of invocations of helpers,
which are constructors or methods declared with the helper modifier
(see section 9.6.4 Semantics of helper methods and constructors).
Thus the post-state of a helper constructor and the pre- and
post-states of helper methods are not visible states.
A state is a visible state for a type T if it occurs after static initialization for T is complete and it is a visible state for some object that has type T. Note that objects of subtypes of type T also have type T.
JML distinguishes static and instance invariants. These are
mutually exclusive and any invariant is either a static or instance
invariant. An invariant may be explicitly declared to be static or
instance by using one of the modifiers static or instance
in the declaration of the invariant. An invariant declared in a class
declaration is, by default, an instance invariant. An invariant
declared in an interface declaration is, by default, a static invariant.
For example, the invariant declared in the class Invariant above
is an instance invariant, because it occurs inside a class declaration.
If Invariant had been an interface instead of a class, then this
invariant would have been a static invariant.
A static invariant may only refer to static fields of an object. An instance invariant, on the other hand, may refer to both static and non-static fields.
The distinction between static and instance invariants also affects when the invariants are supposed to hold. A static invariant declared in a type T must hold in every state that is a visible state for type T. An instance invariant declared in a type T must hold for every object o of type T, for every state that is a visible state for o.
For reasoning about invariants we make a distinction between assuming, establishing, and preserving an invariant. A method (or constructor) assumes an invariant if the invariant must hold in its pre-state. A method or constructor establishes an invariant if the invariant must hold in its post-state. A method or constructor preserves an invariant if the invariant is both assumed and established.
JML's verification logic enforces invariants by making sure that each non-helper method, constructor, or finalizer:
This means that each non-helper constructor found in a class C preserves the static invariants of all types, including C, that have finished their static initialization, establishes the instance invariant of the object under construction, and, modulo creation and deletion of objects, preserves the instance invariants of all other objects. (Objects that are created by a constructor must have their instance invariant established; and objects that are deleted by the action of the constructor can be assumed to satisfy their instance invariant in the constructor's pre-state.) Note in particular that, at the beginning of a constructor invocation, the instance invariant of the object being initialized does not have to hold yet.
Furthermore, each non-helper non-static method found in a type T preserves the static invariants of all types that have finished their static initialization, including T, and, modulo creation and deletion of objects, preserves the instance invariants of all objects, in particular the receiver object. However, finalizers do only assume the instance invariant of the receiver object, and do not have to establish it on exit.
The semantics given above is highly non-modular, but is in general necessary for the enforcement of invariance when no mechanisms are available to prevent aliasing problems, or when constructs like (concrete) public fields are used [Poetzsch-Heffter97]. Of course, one would like to enforce invariants in a more modular way. By a modular enforcement of invariants, we mean that one could verify each type independently of the types that it does not use, and that a well-formed program put together from such verified types would still satisfy the semantics for invariants given above. That is, each type would be responsible for the enforcement of the invariants it declares and would be able to assume, without checking, the invariants of other types it uses.
To accomplish this ideal, it seems that some mechanism for object ownership and alias control [Noble-Vitek-Potter98] [Mueller-Poetzsch-Heffter00] [Mueller-Poetzsch-Heffter00a] [Mueller-Poetzsch-Heffter01a] [Mueller02] [Mueller-Poetzsch-Heffter-Leavens03] is necessary. However, this mechanism is still not a part of JML, although some design work in this direction has taken place [Mueller-Poetzsch-Heffter-Leavens06].
On the other hand, people generally assume that there are no object ownership alias problems; this is perhaps a reasonable strategy for some tools, like run-time assertion checkers, to take. The alternative, tracking which types and objects are in visible states, and checking every applicable invariant for every type and object in a visible state, is obviously impractical.
Therefore, assuming or ignoring the problems with object ownership and alias control, one obtains a simple and more modular way to check invariants. This is as follows.
In this, more modular, style of checking invariants, one can think of all the static invariants in a class as being implicitly conjoined to the pre- and postconditions of all non-helper constructors and methods, and the instance invariants in a class as being implicitly conjoined to the postcondition of all non-helper constructors, and to the pre- and postconditions of all non-helper methods.
As noted above, helper methods and constructors are exempt from
the normal rules for checking invariants. That is because the
beginning and end of invocations of these helper methods and
constructors are not visible states, and therefore they do not have to
preserve or establish invariants. Note that only private
methods and constructors can be declared as helper.
See section 7.1.1.4 Helper Methods and Constructors.
The following subsections discuss other points about the semantics of invariants:
static;
see 8.2.1 Static vs. instance invariants.
public,
protected, and private, or be left with default access;
see 8.2.3 Access Modifiers for Invariants.
requires clauses) specified for that method holds. So
invariants are an integral part of the explanation of method
specifications in 9. Method Specifications.
helper) method or
constructor is invoked. After all, these program points are also
visible states, and, as stated above, invariants should hold at all
visible states.
It should be noted that the last two points above are not specific to Java or JML, but these are tricky issues that have to be considered for any notion of invariant in an object-oriented languages. Indeed, these two issues make the familiar notion of invariant a lot more complicated than one might guess at first sight!
8.2.1 Static vs. instance invariants 8.2.2 Invariants and Exceptions 8.2.3 Access Modifiers for Invariants 8.2.4 Invariants and Inheritance
As discussed above (see section 8.2 Invariants),
invariants can be declared static or instance.
Just like a static method, a static invariant cannot refer to the
current object this and thus cannot refer to instance fields of
this or non-static methods of the type.
Instance invariants must be established by the constructors of an object, and must be preserved by all non-helper instance methods. If an object has fields that can be changed without calling methods (usually a bad idea), then any such changes must also preserve the invariants. For example, if an object has a public field, each assignment to that field must establish all invariants that might be affected.
Static methods do not have a receiver object for which they need to assume or establish an instance invariant, since they have no receiver object. However, a static method may assume instance invariants of other objects, such as argument objects passed to the method.(7)
Static invariants must be established by the static initialization of a class, and must be preserved by all non-helper constructors and methods, i.e., by both static and instance methods.
The table below summarizes this:
| static non-helper non-helper non-helper
| initialization static method constructor instance method
--------------------------------------------------------------------
static | establish preserve preserve preserve
invariant |
|
instance | (irrelevant) (irrelevant) establish preserve,
invariant | if not a
finalizer
|
A word of warning about terminology. As stated above, we call an invariant about static properties "static invariants" and we call an invariant about the dynamic properties of objects an "instance invariant" or, equivalently, an "object invariant." This terminology is contrary to the literature but it is more accurate with respect to the nomenclature of Java.
Methods and constructors should preserve and establish invariants both
in the case of normal termination and in the case of abrupt
termination (i.e., when an exception is thrown). In other words,
invariants are implicitly included in both normal postconditions,
i.e., ensures clauses, and in exceptional postconditions, i.e.,
signals clauses, of methods and constructors.
The requirement that invariants hold after abrupt termination of a method or constructor may seen excessively strong. However, it is the only sound option in the long run. After all, once an object's invariant is broken, no guarantees whatsoever can be made about subsequent method invocations on that object. When faced with a method or constructor that may violate an invariant in case it throws an exception, one will typically try to strengthen the precondition of the method to rule out this exceptional behavior or try to weaken the invariant. Note that a method that does not have any side effects when it throws an exception automatically preserves all invariants.
Invariants can be declared with any one of the Java access modifiers
private, protected, and public. Like class
members, invariants declared in a class have package visibility
if they do not have one of these keywords as modifier. Similarly,
invariants declared in an interface implicitly have public
visibility if they do not have one of these keywords as modifier.
The access modifier of an invariant affects which members, i.e. which fields and which (pure) methods, may be used in it, according to JML's usual visibility rules. See section 2.4 Privacy Modifiers and Visibility, for the details and an example using invariants.
The access modifiers of invariants do not affect the obligations
of methods and constructors to maintain and establish them. That is,
all non-helper methods are expected to preserve
invariants irrespective of the access modifiers of the invariants and
the methods. For example, a public method must preserve private
invariants as well as public ones.
As noted in See section 2.4 Privacy Modifiers and Visibility, there are restrictions on the visibility of fields that can be referenced in invariants to prevent specifications that clients cannot understand and to prevent invariants that clients cannot preserve. Thus, for example, private invariants cannot mention public fields [Leavens-Mueller07].
Each type inherits all the instance invariants specified in its superclasses and superinterfaces. [[[Erik wrote: "Static invariants are not inherited", but there seems to be some kind of static field inheritance in Java...]]] [[[ DRCok- but all the static invariants of a superclass have to be maintained by the subclass methods - isn't this equivalent to inheritance?]]]
The fact that (instance) invariants are inherited is one of the
reasons why the use of the keyword super is not allowed
in invariants. [[[ Is this true? - I don't understand this. DRCok ]]]
History constraints [Liskov-Wing93b] [Liskov-Wing94], which we call constraints for short, are related to invariants. But whereas invariants are predicates that should hold in all visible states, history constraints are relationships that should hold for the combination of each visible state and any visible state that occurs later in the program's execution. Constraints can therefore be used to constrain the way that values change over time.
The syntax of history constraints in JML is as follows.
history-constraint ::= constraint-keyword predicate
[ |
Because methods will not necessarily change the values referred to in a constraint, a constraint will generally describe reflexive and transitive relations.
For example, the constraints in the example below say that the
value of field a and the length of the array b will
never change, and that the length of the array c will only ever
increase.
package org.jmlspecs.samples.jmlrefman;
public abstract class Constraint {
int a;
//@ constraint a == \old(a);
boolean[] b;
//@ invariant b != null;
//@ constraint b.length == \old(b.length) ;
boolean[] c;
//@ invariant c != null;
//@ constraint c.length >= \old(c.length) ;
//@ requires bLength >= 0 && cLength >= 0;
Constraint(int bLength, int cLength) {
b = new boolean[bLength];
c = new boolean[cLength];
}
}
|
\old.
A constraint declaration may optionally explicitly list one or more methods. It is the listed methods that must respect the constraint. If no methods are listed, then all non-helper methods of the class (and any subclasses) must respect the constraint. A method respects a history constraint iff the pre-state and the post-state of a non-static method invocation are in the relation specified by the history constraint. So one can think of history constraints as being implicitly included in the postcondition of relevant methods. However, history constraints do not apply to constructors and destructors, since constructors do not have a pre-state and destructors do not have a post-state.
Private methods declared as helper methods do not have to
respect history constraints, just like these do not have to preserve
invariants.
A few points to note about history constraints:
static;
see 8.3.1 Static vs. instance constraints.
public,
protected, and private;
see 8.3.2 Access Modifiers for Constraints.
requires clauses) specified for that method holds. So
constraints are an integral part of the explanation of method
specifications in 9. Method Specifications.
helper) methods or constructors are invoked are also
visible states, constraints should also hold between the pre-state and
any such program points, between these program points themselves, and
between any such program points and the post-state.
o should not just respect the
constraints of o, but should respect the constraints of all
other (reachable) objects as well.
These aspects of constraints are discussed in more detail below.
8.3.1 Static vs. instance constraints 8.3.2 Access Modifiers for Constraints 8.3.3 Constraints and Inheritance
History constraints can be declared static.
Non-static constraints are also called instance constraints.
Like a static invariant, a static history constraint cannot refer to the
current object this or to its fields.
Static constraints should be respected by all constructors and all methods, i.e., both static and instance methods.
Instance constraints must be respected by all instance methods.
The table below summarizes this:
| static non-helper non-helper non-helper
| initialization static method constructor instance method
--------------------------------------------------------------------
static | (irrelevant) respect respect respect
constraint|
|
instance | (irrelevant) (irrelevant) (irrelevant) respect
constraint|
|
Instance constraints are irrelevant for constructors, in that here there is no pre-state for a constructor that can be related (or not) to the post-state. However, if a visible state arises during the execution of a constructor, then any instance constraints have to be respected.
In the same way, and for the same reason, static constraints are irrelevant for static initialization.
The access modifiers public, private, and protected
pose exactly the same restrictions on constraints as they do on invariants,
see 8.2.3 Access Modifiers for Invariants.
Any class inherits all the instance constraints specified in its superclasses and superinterfaces. [[[Static constraints are not inherited.]]] [[[ But they still apply to subclasses, no ? and it says they are above - David]]]
The fact that (instance) constraints are inherited is one of the
reasons why the use of the keyword super is not allowed
in constraints. [[[ Needs explanation - David ]]]
The following is the syntax for represents clauses.
represents-clause ::= represents-keyword store-ref-expression |
The first form of represents clauses is called a functional abstraction. This form
defines the value of the store-ref-expression in a visible state
as the value of the spec-expression that follows the =.
The second form (with \such_that) is called a
relational abstraction.
This form constrains the value of the store-ref-expression in a
visible state to satisfy the given predicate.
represents clause must be a reference
to a model field (See section 7. Class and Interface Member Declarations, for details of model fields). Although it is a store-ref-expression,
wild cards and array ranges are not permitted.
boolean.
For each type and model field, there
can be at most one non-redundant represents-clause
that in the type that has the given model field in its left-hand side.
A represents clause is redundant if
it is introduced using the keyword represents_redundantly.
A represents-clause can be declared as static
(See section 6. Type Declarations, for static declarations). In a
static represents clause, only static elements can be
referenced both in the left-hand side and the right-hand side. In
addition, the following restriction is enforced:
static represents clause must be declared in the type
where the model field on the left-hand side is declared.
Unless explicitly declared as static, a represents-clause
is non-static (for exceptions see see section 6. Type Declarations).
A non-static represents clause can refer to
both static and non-static elements on the right-hand
side.
static represents clause must not have a static model
field in its left-hand side.
static represents clause must be declared in a type
descended from (or nested within) the type where the model field on
the left-hand side is declared.
Note that represents clauses can be recursive. That is, a represents clause may name a field on its right hand side that is the same as the field being represented (named on the left hand side). It is the specifier's responsibility to make sure such definitions are well-defined. But such recursive represents clauses can be useful when dealing with recursive datatypes [Mueller-Poetzsch-Heffter-Leavens03].
The initially-clause has the following syntax.
initially-clause ::= |
The meaning of an initially-clause is that each non-helper (see section 6.2.9 Helper) constructor for each concrete subtype of the enclosing type (including that type itself, if it is concrete) must establish the predicate. Thus, the predicate can be thought of as implicitly conjoined to the postconditions of all non-helper constructors of such a type and all of its subtypes.
An axiom-clause has the following syntax.
axiom-clause ::= |
Such a clause specifies that a theorem prover should assume that the given predicate is true (whenever such an assumption is needed).
[[[ example needed ]]]
The syntax of the readable-if-clause is as follows.
readable-if-clause ::= |
Such a clause gives a condition that must be true before the field named by ident can be read. This field must be one declared in the type in which the declaration appears, or in a supertype of the class.
The syntax of the writeable-if-clause is as follows.
writable-if-clause ::= |
Such a clause gives a condition that must be true before the field named by ident can be written. This field must be one declared in the type in which the declaration appears, or in a supertype of the class.
The monitors-for-clause is adapted from ESC/Java [Leino-Nelson-Saxe00] [Rodriguez-etal05]. It has the following syntax.
monitors-for-clause ::= |
A monitors-for-clause such as monitors_for f <- e1, e2;
specifies a relationship between the field, f
and a set of objects, denoted by a specification expression list
e1, e2. The meaning of this declaration is
that all of the (non-null) objects in the list, in this
example, the objects denoted by e1 and e2, must be
locked to read the field (f in the example) in this object.
Note that the righthand-side of the monitors-for-clause is not just a store-ref-list, but is in fact a spec-expression-list, where each spec-expression evaluates to a reference to an object.
| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |