| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This chapter discusses fundamental concepts that are used in explaining the semantics of JML.
In this manual we use type to mean either a class, interface, or
primitive value type in Java. (Primitive value types include
boolean, int, etc.)
A reference type is a type that is not a primitive value type, that is either a class or interface. When it is not necessary to emphasize that primitive value types are not included, we often shorten "reference type" to just "type".
In JML one can declare various names with the modifier model; for
example one can declare as "model" fields, methods, and even types.
One can also declare some fields as ghost fields.
JML also has a model import directive (see section 5. Compilation Units).
The model modifier has two meanings.
The first meaning of a feature declared with model is that it is only
present for specification purposes. For example a model field is an
imaginary field that is only used for specifications and is not
available for use in Java code outside of annotations.
Similarly, a model method is a method that can be used in annotations,
but cannot be used in ordinary Java code. A model import directive
imports names that can be used only within JML annotations.
The second meaning of model depends on the type of feature
being declared.
The most common and useful model declarations are model fields.
A model field should be thought of as the abstraction of one or more
non-model (i.e., Java or concrete) fields [Cheon-etal05].
(By contrast, some authors refer to what JML calls model fields as
"abstract fields" [Leino98].)
The value of a model field is determined by the concrete fields it
abstracts from; in JML this relationship is specified by a
represents clause (see section 8.4 Represents Clauses).
(Thus the values of the model fields in an object determines its
"abstract value" [Hoare72a].)
A model field also defines a data group [Leino98],
which collects model and concrete fields and is used to tell JML what
concrete fields may be assigned by various methods (see section 10. Data Groups).
Unlike model fields, model methods and model types are not abstractions of non-model methods or types. They are simply methods or types that we imagine that the program has, to help in a specification.
A ghost field is similar to a model field, in that it is
also only present for purposes of specification and thus cannot be
used outside of JML annotations.
However, unlike a model field, a ghost field does not have a value
determined by a represents clause; instead its value is directly
determined by its initialization or by a set-statement
(see section 13. Statements and Annotation Statements).
Although these model and ghost names are used only for specifications,
JML uses the same namespace for such names as for normal Java names.
Thus, one cannot declare a field to be both a model (or ghost) field and
a normal Java field in the same class
(see section 17. Separate Files for Specifications).
Similarly, a method is either a model method or not.
In part, this is done because JML has no syntactic distinction between
Java and JML field access or method calls.
This decision makes it an error for someone to use the same name as a
model or ghost feature in an implementation.
In such a case if the Java code is considered to be the eventual goal,
then one can either change the name of the JML feature
or have one declaration in which
the Java feature is modified with the JML modifier spec_public.
See section 2.4 Privacy Modifiers and Visibility, for more about spec_public.
In JML one is not required to specify behavior completely. Indeed, JML has a style of method specification case, called lightweight, in which the user only says what interests them. On the other hand, in a heavyweight specification case, JML expects that the user is fully aware of the defaults involved. In a heavyweight specification case, JML expects that a user only omits parts of the specification case when the user believes that the default is appropriate.
Users distinguish these between such cases of method specifications by
using different syntaxes. See section 9.2 Organization of Method Specifications,
for details, but in essence in a method specification case that
uses one of the behavior keywords (such as normal_behavior,
exceptional_behavior, or behavior) is heavyweight,
while one that does not use such a keyword is lightweight.
Java code that is not within a JML annotation uses the usual access control
rules for
determining visibility (or accessibility) of Java [Arnold-Gosling-Holmes00]
[Gosling-etal00].
That is, a name declared in package P and type P.T
may be referenced from outside P
only if it is declared as public,
or if it is declared as protected
and the reference occurs within a subclass of P.T.
This name may be referenced from within P
but outside of P.T
only if it is declared as public, default access,
or protected.
Such a name may always be referenced from within P.T,
even if it is declared as private.
See the Java language specification [Gosling-etal00]
for details on visibility rules
applied to nested and inner classes.
Within annotations, JML imposes some extra rules in addition
to the usual Java visibility rules [Leavens-Baker-Ruby06] [Leavens-Mueller07].
These rules depend not just on the declaration of the name but also on
the visibility level of the context that is referring to the name in
question.
For purposes of this section, the annotation context of a
reference to a name is the smallest grammatical unit with an attached
(or implicit) visibility. For example, this annotation context could
be a method specification case, an invariant, a history constraint,
or a field declaration.
The visibility level of such an annotation context can be public,
protected, private, or default (package) visibility.
JML has two rules governing visibility that differ from Java. The first is that an annotation context cannot refer to names that are more hidden than the context's own visibility. That is, for a reference to a name x to be legal, the visibility of the annotation context that contains the reference to x must be at least as permissive as the declaration of x itself. The reason for this restriction is that the people who are allowed to see the annotation should be able to see each of the names used in that annotation [Meyer97], otherwise they might not understand it. For example, public clients should be able to see all the declarations of names in publicly visible annotations, hence public annotations should not contain protected, default access, or private names.
In more detail, suppose x is a name declared in package P and type P.T.
public
(or spec_public).
public
or protected, and x must also be visible according to
Java's rules (so if x is protected, or spec_protected,
then the reference must either be from within P
or, if it is from outside P,
then the reference must occur in a subclass of P.T).
public,
protected, or with default visibility,
and x must also be visible according to
Java's rules (so if x has default visibility,
then the reference must be from within P).
private visibility annotation context
(e.g., in a private method specification)
can refer to x only if x is visible according to
Java's rules (so if x has private visibility,
then the reference must be from within P.T).
In the following example, the comments on the right show which uses of the various privacy level names are legal and illegal. Similar examples could be given for method specifications, history constraints, and so on.
public class PrivacyDemoLegalAndIllegal {
public int pub;
protected int prot;
int def;
private int priv;
//@ public invariant pub > 0; // legal
//@ public invariant prot > 0; // illegal!
//@ public invariant def > 0; // illegal!
//@ public invariant priv < 0; // illegal!
//@ protected invariant prot > 1; // legal
//@ protected invariant def > 1; // illegal!
//@ protected invariant priv < 1; // illegal!
//@ invariant def > 1; // legal
//@ invariant priv < 1; // illegal!
//@ private invariant priv < 1; // legal
}
|
Note that in a lightweight method specification, the privacy level is assumed to be the same privacy level as the method itself. That is, for example, a protected method with a lightweight method specification is considered to be a protected annotation context for purposes of checking proper visibility usage [Leavens-Baker-Ruby06] [Mueller02]. See section 2.3 Lightweight and Heavyweight Specifications, for more about the differences between lightweight and heavyweight specification cases.
(The ESC/Java2 system has the same visibility rules as described above. However, this was not true of the old version of ESC/Java [Leino-Nelson-Saxe00].)
The JML keywords spec_public and spec_protected provide
a way to make a declaration
that has different visibilities for Java and JML. For example, the
following declaration declares an integer field that Java regards as
private but JML regards as public.
private /*@ spec_public @*/ int length; |
Thus, for example, length in the above declaration
could be used in a public method specification or invariant.
However, spec_public is more than just a way to change the
visibility of a name for specification purposes. When applied to
fields it can be considered to be shorthand for the declaration of a
model field with a similar name. That is, the declaration of length
above can be thought of as equivalent to the following
declarations, together with a rewrite of the Java code that uses
length to use _length instead
(where we assume _length is fresh, i.e., not used elsewhere in
the class).
//@ public model int length; private int _length; //@ in length; //@ private represents length = _length; |
The above desugaring allows one to change the underlying field without affecting the readers of the specification.
The desugaring of spec_protected is the same as for
spec_public, except that one uses protected
instead of public in the desugared form.
The second rule for visibility prohibits an annotation context from writing specifications in an annotation context that constrain fields that are visible to more clients than the specifications (see section 3 of [Leavens-Mueller07]). In particular, this applies to invariants and history constraints. Thus, for example, a private invariant cannot mention a public field, since clients could see the public field without seeing the invariant, and thus would not know when they might violate the private invariant by assigning to the public field. Thus, for example, the invariants in the following example are all illegal, since they constrain fields that are more visible than the invariant itself.
public class PrivacyDemoIllegal {
public int pub;
protected int prot;
int def;
private int priv;
//@ protected invariant pub > 1; // illegal!
//@ invariant pub > 1; // illegal!
//@ invariant prot > 1; // illegal!
//@ private invariant pub > 1; // illegal!
//@ private invariant prot > 1; // illegal!
//@ private invariant def > 1; // illegal!
}
|
In Java, a feature of a class or interface may declared to be
static. This means that the feature is not part of instances
of that type, and it means that references to that feature (from
outside the type and its subtypes) must use a qualified name of the
form T.f, which refers to the static feature f in type T.
A feature, such as a field or method, of a type that is not static is
an instance feature. For example, in a Java interface, all the
methods declared are instance methods, although fields are static by
default. In a Java class the default is that all features are
instance features, unless the modifier static is used.
In JML declarations follow the normal Java rules for determining
whether they are instance or static features of a type. However,
within annotations it is possible to explicitly label features as
instance (see section 6. Type Declarations for the syntax).
The use of the instance modifier is necessary to declare model
and ghost instance fields in interfaces, since otherwise the Java
default modifier for fields in interfaces (static) would apply.
It is also useful, in JML, to label invariants as either static or instance invariants. See section 8.2.1 Static vs. instance invariants, for more on this topic.
A location is a field of an object or a local variable. A local variable is either a variable declared inside a block (such as a method body) or a formal parameter of a method.
An access path is an expression either of the form x, where
x is an identifier, or p.x, where p is an access
path and x is an identifier.(5)
(In forming an access path, we ignore visibility.)
In a given program state, s, a location l is aliased if there are two or more access paths that, in s, both denote l. The access paths in question are said to be aliases for l. Similarly, we say that an object o is aliased in a state s if there are two access paths that, in s, both have o as their value. In Java, it is impossible to alias local variables, so the only aliasing possible involves objects and their fields.
Within JML annotations, Java expressions generally have the values that are defined in the Java Language Specification [Gosling-etal00]. This has consequences on the interpretation of assertion expressions [Chalin07] [Rioux-Chalin07]: an assertion is taken to be valid if and only if its interpretation
true.
The strong validity semantics for assertion evaluation means that exceptions may arise during evaluation of subexpressions within assertions. These exceptions should be avoided by the specifier and tools are encouraged to warn users when they detect that an exception may arise during assertion evaluation.
To avoid exceptions during assertion evaluation, specifiers should
practice good Java coding habits, and write specifications that
prevent such exceptions.
To do this, one can use left-to-right ordering of evaluation of
subexpressions and the short-curcuit nature of the Java
operators && and ||.
JML also evaluates the its two implication operators,
==> and <== in short-curcuit fashion from left to right.
Within a specification case, the precondition can
protect the rest of the specification from exceptions
[Leavens-Wing98].
That is, one can assume that the precondition holds in the remainder
of the clauses in a specification case.
JML also evaluates multiple occurrences of clauses of the same kind
(such as requires or ensures) within a spec case in top
to bottom order, so earlier clauses can protect later ones, just as if they
were combined with &&.
One common problem that occurs in Java and JML specifications
is the possibility of null dereferences. For example,
if x is null then x.f and x.m() both
result in a NullPointerException.
Such null pointer exceptions cause undefinedness
in expression evaluation, as described above
(see section 2.7 Expression Evaluation and Undefinedness).
To avoid having to constantly specify that declarations (other than
local variables) are non-null, JML makes them implicitly non_null by default.
That is, unless a
nullable, that declaration is assumed to be non_null.
For a field whose type is an array of reference types, such as a field
of type Object[], both the field that refers to the array and
the elements of the array are non_null by default.
If a field whose type is an array of reference types is declared as
nullable, then both the reference to the array and all of its
elements may potentially be null. To specify that the field is not
null but the elements may be null, use an invariant to state that the
field cannot contain null, as follows.
private /*@ spec_public nullable @*/ Object[] a; //@ public invariant a != null; |
While these defaults differ from Java, research has found that in most cases a declaration is expected to be non-null [Chalin-Rioux05]. More importantly, since one of the most common mistakes in JML specifications (and in Java programs) is forgetting to specify that a declaration is non-null, making the default be that they cannot hold null helps eliminate a source of common errors in specifications.
See section 6.2.13 Nullity Modifiers, for more details on the nullity modifiers.
One of JML's goals is to provide a single language that can be used with a variety of different tools. However, JML is also an evolving language that is used as a research vehicle by many groups. The evolution of JML means that some features are not completely documented or implemented. Use of JML in research means that some tools will have features that are not supported by other tools. All of this has the potential to threaten portability and to make JML more difficult to learn and use.
The research groups working on JML are committed to making these problems as invisible to non-researchers as possible, and for this reason have defined several language levels. The goal of defining these language levels is to make it easier to learn and use JML and its various tools.
We define the following language levels.(6)
When learning JML, one should focus on levels 0 features first, as these form the heart of the language which should be understood by all JML tools. Features at level 1 are next in importance and should be supported by most tools that are interested in having a large user base. Features at higher levels are less important and may not be present in all tools. Users should feel free to ignore them unless they meet some specific need.
The language levels also provide guidance for tool designers. JML tools should parse all of the syntax in this reference manual that is not marked as experimental. This is the most important way to guarantee portability for users, and the easiest way for tools to get feedback. In addition, tools should check at least level 0, and preferably level 1 features. Features at levels 2 and 3 are candidates for the tool to just parse and ignore, if they are not features of interest for that tool. Experimental features may ignored (or added) by any tool.
Many tool developers may want to start off supporting only a subset of JML defined by level 0 and then move on to higher levels.
It is also suggested that tools give users optional feedback, perhaps in a verbose mode, as to which features are fully and partially supported. Clearly stating which JML levels are supported in a tool release is also very important.
More details are provided in the subsections below.
2.9.1 Level 0 Features 2.9.2 Level 1 Features 2.9.3 Level 2 Features 2.9.4 Level 3 Features 2.9.5 Level C Features 2.9.6 Level X Features
The features in this level form the core of JML and should be understood and checked by all JML tools. Beginning users should pay the most attention to these features. These features include all of Java and the syntax described in the rest of this section.
Synonyms for the keywords used in level 0 features are also considered
to be part of level 0's lexical syntax.
For example, since assignable is a
keyword used in level 0, its synonyms modifiable and
modifies are also included in the lexical syntax for level 0.
Many, but not all, of the JML additions to Java's modifiers (see section 6.2 Modifiers) are level 0 features. The following modifiers are included in level 0.
spec_public (see section 6.2.3 Spec Public).
spec_protected (see section 6.2.4 Spec Protected).
instance (see section 6.2.8 Instance).
model (see section 6.2.6 Model), as applied to field
declarations (see section 7.1.2.1 JML Modifiers for Fields).
Note that this modifier as applied to other
declarations is not a level 0 feature.
ghost (see section 6.2.7 Ghost), as applied to both
field and variable declarations (see section 7.1.2 Field and Variable Declarations).
helper (see section 6.2.9 Helper).
Type specifications (see section 8. Type Specifications) are a level 0 feature, although not all clauses and features of type specifications are level 0. The following type-level clauses are included in level 0.
instance (see section 6.2.8 Instance) or one that is
written in a class and that does not use the modifier static
(see section 8.2.1 Static vs. instance invariants).
= and (not \such_that).
\TYPE (optionally, as a type of array
element).
See section 7.1.2.2 Type-Specs, for more details.
Method specifications (see section 9. Method Specifications) are a level 0
feature.
This includes the ability to combine specification cases using
also
(see section 9.6.5 Semantics of nested behavior specification cases)
and specification inheritance [Dhara-Leavens96] [Leavens-Naumann06] [Leavens06b].
It also includes the use of \not_specified for all
specification clauses that are at level 0.
However, not all clauses and features of method
specifications are level 0. The following parts of method
specifications are included in level 0.
Redundancy features of method specifications are only present at
level 1, not at level 0. The details are described below.
code.
This includes
behavior-spec-case (see section 9.6 Behavior Specification Cases),
normal-behavior-spec-case
(see section 9.7 Normal Behavior Specification Cases),
and
exceptional-behavior-spec-case
(see section 9.8 Exceptional Behavior Specification Cases).
However, note that not all clauses that are allowed in the syntax are
in level 0.
requires_redundantly, pre_redundantly) is a level 1 feature.
ensures_redundantly, post_redundantly) is a level 1 feature.
signals_redundantly, exsures_redundantly) is a level 1 feature.
signals_only_redundantly) is a level 1 feature.
assignable_redundantly, modifiable_redundantly,
modifies_redundantly) is a level 1 feature.
Only static data groups (see section 10. Data Groups) are part of level 0.
Some of JML's extensions to Java's expression syntax (see section 12. Predicates and Specification Expressions), but not all of them, can be used at level 0. Note that calls to pure methods and constructors in spec-expressions are not part of level 0, but are only found at level 1. We describe the level 0 specification expressions below.
\result).
\old and \pre).
\fresh).
\nonnullelements).
\typeof).
\elemtype).
\type).
\forall and \exists
(see section 12.4.24.1 Universal and Existential Quantifiers).
(The quantifier keywords
\max, \min, \product, and \sum
(see section 12.4.24.2 Generalized Quantifiers), as well as \num_of
(see section 12.4.24.3 Numerical Quantifier, are all level 1 features.)
<: operator (see section 12.6.1 Subtype operator).
<==> and <=!=> operators
(see section 12.6.2 Equivalence and Inequivalence Operators).
==> and <== operators
(see section 12.6.3 Forward and Reverse Implication Operators).
All of the Java statements and most of the JML extensions for adding assertions to statements and annotation statements (see section 13. Statements and Annotation Statements) are at level 0. But redundancy features of the JML extensions are only present at level 1, not at level 0. We describe the level 0 extensions to Java statements below.
ghost in local-declarations
(see section 13.1.1 Modifiers for Local Declarations).
maintaining_redundantly and
loop_invariant_redundantly are level 1 features.
Furthermore, the variant-function is a level 1 feature.
assert_redundantly, is in level 1.
assume_redundantly is a level 1 feature.
The ability to
use a .jml file (see section 17.1 File Name Suffixes)
to give a separate specification for a
compilation unit that only appears in binary form (e.g., in a
.class file) is a level 0 feature.
Some syntax from the Universe type system
(see section 18. Universe Type System) is included in level 0.
However, readonly is considered to be in level X, as is the semantics
of the Universe type system. The rep and peer modifiers
are included in level 0 because, in some form, they are important to
the semantics of several level 0 features
[Mueller-Poetzsch-Heffter-Leavens03] [Mueller-Poetzsch-Heffter-Leavens06].
\rep and rep ownership-modifiers
(see section 18.2 Rep and Peer).
\peer and peer ownership-modifiers
(see section 18.2 Rep and Peer).
The features in this level will be understood and checked by many JML tools. They are quite important in practice, especially the use of methods and constructors in writing the specifications of other methods and constructors. Also useful are all of JML's redundancy features (see section 14. Redundancy), which are included here for all level 0 features and for other features at level 1.
The following additions to Java's modifiers (see section 6.2 Modifiers) are level 1 features.
model (see section 7.1.1.2 Model Methods and Constructors).
However, note that using model on a field
declarations is a level 0 feature and that using model on a
type declaration is a level 3 feature.
model
(see section 5.2 Import Declarations).
pure (see section 6.2.5 Pure).
uninitialized (see section 6.2.11 Uninitialized).
The following type-level clauses (see section 8. Type Specifications) are included in level 1.
instance (see section 6.2.8 Instance), or one that is
written in a class and that uses the modifier static
(see section 8.2.1 Static vs. instance invariants).
The following features of method specifications (see section 9. Method Specifications) are included in level 1.
implies_that) part of a redundant-spec
(see section 14.1 Redundant Implications and Redundantly Clauses).
for_example) part of a redundant-spec.
The following extensions to Java's expression syntax (see section 12. Predicates and Specification Expressions) are included in level 1.
\max, \min, \product, and \sum
(see section 12.4.24.2 Generalized Quantifiers), as well as \num_of
(see section 12.4.24.3 Numerical Quantifier).
(Note that the \max quantifier is distinct from the
max-expression (see section 12.4.20 \max), which is a level C
feature.
Also, note that the quantifier keywords \forall and
\exists are level 0 features.)
The following additions to Java's statement syntax (see section 13. Statements and Annotation Statements) are included in level 1.
maintaining_redundantly and
loop_invariant_redundantly.
Non-redundant loop-invariants are in level 0.
assert_redundantly.
The non-redundant assert-statements are a level 0 feature.
assume_redundantly.
The non-redundant assume-statements are a level 0 feature.
The \bigint type (see section 19.1 \bigint)
from the safe math extensions (see section 19. Safe Math Extensions) is a level 1
feature.
Level 2 contains features that are more specialized to particular uses of JML, but are still useful for several different tools. It also contains some features that are mainly needed to explain JML's semantics, and have not been heavily used (so far).
The nowarn-pragma (see section 4.2 Lexical Pragmas).
The following type-level clauses (see section 8. Type Specifications) are included in level 2.
\such_that.
Note that the functional form of such represents clauses is a level 0
feature.
The following features of method specifications (see section 9. Method Specifications) are included in level 2.
extract modifier (see section 15.2 Extracting Model Program Specifications).
The following extensions to Java's expression syntax (see section 12. Predicates and Specification Expressions) are included in level 2.
\not_assigned).
\not_modified).
\only_accessed).
\only_assigned).
\only_called).
\only_captured).
\reach).
\is_initialized).
\invariant_for).
\lblneg and \lblpos).
The following additions to Java's statement syntax (see section 13. Statements and Annotation Statements) are included in level 2.
Note that all the model-prog-statements (see section 15. Model Programs) are at level 2, because the model program style of method specification is at this level.
Aside from the \bigint type (see section 19.1 \bigint),
which is a level 1 feature, the rest of the safe math extensions
(see section 19. Safe Math Extensions) are level 2
features. This includes the following particulars.
\real type (see section 19.2 \real).
code_bigint_math, code_java_math,
code_safe_math, spec_bigint_math,
spec_java_math, and spec_safe_math (see section 6.2.12 Math Modifiers).
Level 3 features are more exotic and even less commonly used. The semantics of some of these features are not yet well understood, and the features are not implemented by many tools.
model
(see section 6.1.2 Modifiers for Type Declarations).
\duration).
\space).
\working_space).
The features in this level are related to the specification of concurrency. This includes features inherited from ESC/Java having to do with concurrency. The features of this level are as follows.
\lockset).
\max). Note that this is
not the quantifier \max
(see section 12.4.24.2 Generalized Quantifiers), which is a level 1 feature.
<# and <=# operators applied to test ordering of locks
(see section 12.6.4 Lockset Ordering).
The features in this level are experimental. Some of the ones we know about are as follows.
\readonly and readonly ownership-modifiers
from the Universe type system (see section 18. Universe Type System).
Note that the \peer and \rep modifiers are level 0 features.
| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |