|[Top]||[Contents]||[Index]||[ ? ]|
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.
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.
pre can also be used as a synonym for
post can also be used as a synonym for
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
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
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
For compatibility with ESC/Java, JML also supports the tags
Because the current ESC/Java2 tool does not
the specification uses uses annotation markers
These markers are understood by the ISU JML tools, but are considered to
be comments by ESC/Java2.
jmldoc tool is generously provided by David Cok; thanks David!.
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.
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.
x is not
the same object as
Thanks to Erik Poll for discussions on checking of assignable clauses.
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 22.214.171.124 Data Groups and Represents Clauses, for more on this subject.
The keyword "
exsures" can also be used in place of
Of course, one could specify
separating out the interface
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.
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
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].
Thanks to Erik Poll for pointing this out.
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.
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
One may also give
which are analogous to
example clauses, which are analogous to
There is also a lightweight form of example, this is
similar to the
example form, except that the introductory keywords
public example" are omitted.
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.
represents clause is implicitly an instance, as opposed to
a static, represents clause, because it appears in a class
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
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.
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.
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.
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.
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