Footnotes

(1)

In JML method specifications must be placed either before the method's header, as shown above, or between the method's header and its body. In this document, we always place the specification before the method header. This convention is followed by many Java tools, in particular by Javadoc; It has the advantage of working in all cases, even when the method has no body.

(2)

In a protected specification, both public and protected identifiers can be used. In a specification with default (i.e., no) visibility specified, which corresponds to Java's default visibility, public and protected identifiers can be used, as well as identifiers from the same package with default visibility. A private specification can use any identifiers that are available. The privacy level of a method specification cannot allow more access than the method being specified. Thus a public method may have a private specification, but a private method may not have a public specification.

(3)

The keyword pre can also be used as a synonym for requires.

(4)

The keyword post can also be used as a synonym for ensures.

(5)

The result plus one squared will become negative if the result is larger than 46340, due to integer overflow. Patrice Chalin pointed out that in an earlier version of this specification there were overflow problems [Chalin02]. In Java integer arithmetic, one plus the maximum integer is the minimum integer. This specification deals with such problems by limiting the result to be a positive integer and by the implication on lines 8-9. See the specification of IntMathOps2 below for another way to deal with these problems.

(6)

Since HTML tags are not case sensitive, in this one place JML is also not case sensitive. That is, the syntax also permits the tags <JML>, </JML>. For compatibility with ESC/Java, JML also supports the tags <esc>, </esc>, <ESC>, and </ESC>.

(7)

Because the current ESC/Java2 tool does not understand spec_bigint_math mode, the specification uses uses annotation markers /*+@ and @+*/. These markers are understood by the ISU JML tools, but are considered to be comments by ESC/Java2.

(8)

The jmldoc tool is generously provided by David Cok; thanks David!.

(9)

In JML invariants also apply to non-public methods as well. The only exception is that a private method or constructor may be marked with the helper modifier; such methods cannot assume and do not need to establish the invariant.

(10)

For historical reasons, one can also use the keyword modifiable as a synonym for assignable. Also, for compatibility with (older versions of) ESC/Java [Leino-etal00], in JML, one can also use the keyword modifies as a synonym for assignable. In the literature, the most common keyword for such a clause is modifies, and what JML calls the "assignable clause" is usually referred to as a "modifies clause". However, in JML, "assignable" most closely corresponds to the technical meaning, so we use that throughout this document. Users of JML may write whichever they prefer, and may mix them if they please.

(11)

Assuming that x is not the same object as this!

(12)

Thanks to Erik Poll for discussions on checking of assignable clauses.

(13)

Furthermore, static model fields must have concrete implementations in the interfaces in which they are declared, if they are to have any representation at all. See section 2.2.2.1 Data Groups and Represents Clauses, for more on this subject.

(14)

The keyword "exsures" can also be used in place of signals.

(15)

Of course, one could specify BoundedStackInterface without separating out the interface BoundedThing, and in that case, these layers would be unnecessary. We have made this separation partly to demonstrate more advanced features of JML, and partly to make the parts of the example smaller.

(16)

Note that the permission to assign a field goes from the more abstract field to the one in its group (which in this case is also abstract). Müller points out that this direction is necessary for information hiding, because concrete fields are often hidden (e.g., they may be private), and as such cannot appear in public specifications, so the public specification has to mention the more abstract field, which give assignment rights to its members [Mueller02].

(17)

Thanks to Erik Poll for pointing this out.

(18)

Meyer's second specification and implementation of stacks (see page 349 of [Meyer97]) is no better in this respect, although, of course, the implementation does keep track of the elements properly.

(19)

There is no use of initially in this interface, so data type induction cannot assume any particular starting value. But this is desirable, since if a particular starting value was specified, then by the history constraint, all objects would have that value.

(20)

One may also give exceptional_example clauses, which are analogous to exceptional_behavior specifications, and example clauses, which are analogous to behavior specifications. There is also a lightweight form of example, this is similar to the example form, except that the introductory keywords "public example" are omitted.

(21)

Observable aliasing is a sharing relation between objects that can be detected by a program. Such a program, might, for example modify one object and read a changed value from the shared object. Formalizing this in general is beyond the scope of this paper, and probably beyond what JML can describe.

(22)

This represents clause is implicitly an instance, as opposed to a static, represents clause, because it appears in a class declaration.

(23)

As of JDK 1.4, assert is also a reserved word in Java. One can thus write assert statements either in standard Java or in JML annotations. If one writes an assert statement as a JML annotation, all of the JML extensions to the Java expression syntax see section 3.1 Extensions to Java Expressions for Predicates for the predicate can be used, but no side-effects are allowed in this predicate. Such a JML assert-statement may also refer to model and ghost variables. In a Java assert statement, i.e., in an assert-statement that is not in an annotation, one cannot use JML's extensions for assertions, because such assertions must compile with a Java compiler.

(24)

When such private and default visibility specification cases are visible to callers, they may only be used in verification of a method call if the call can be shown to be executing that method, as opposed to some override.

(25)

However, textual copying shouldn't be taken literally; if a subclass declares a field that hides the fields of its superclass, renaming must be done to prevent name capture.

(26)

Suppose A is the superclass of B, and B is the superclass of C. Suppose B's specification used super to call a method of A. The problem is that when this specification is inherited by C, if we imagine copying B's specification to C, then this use of super no longer refers to A, but to B. Thanks to Arnd Poetzsch-Heffter for pointing out this problem.

(27)

Note that it is wrong to use \fresh(this) in the specification of a constructor, because Java's new operator allocates storage for the object; the constructor's job is just to initialize that storage.