| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The following is the syntax of type declarations.
type-declaration ::= class-declaration
| interface-declaration
| |
The specification of a type-declaration is determined as follows.
If the type-declaration consists only of a semicolon (;),
then the specification is empty. Otherwise the specification is that
of the class or interface declaration. Such a specification must be
satisfied by the corresponding class or interface declaration.
The rest of this chapter discusses class and interface declarations, as well as the syntax of modifiers.
6.1 Class and Interface Declarations 6.2 Modifiers
Class and interface declarations are quite similar, as interfaces may be seen as a special kind of class declaration that only allows the declaration of abstract instance methods and final static fields (in the Java code, see Chapter 9 of [Gosling-etal05]). Their syntax is also similar.
class-declaration ::= [ doc-comment ] modifiers |
Documentation comments for classes and interfaces may not contain JML specification information. See section 4.5 Documentation Comments, for the syntax of documentation comments.
See section 7. Class and Interface Member Declarations, for the syntax and semantics of fields, which form the essence of classes and interfaces.
The rest of this section discusses subtyping for classes and interfaces and also the particular modifiers used in classes and interfaces.
6.1.1 Subtyping for Type Declarations 6.1.2 Modifiers for Type Declarations
Classes in Java can use single inheritance and may also implement any number of interfaces. Interfaces may extend any number of other interfaces.
class-extends-clause ::= [ |
The meaning of inheritance in JML is similar to that in Java. In Java, a when class S names a class T in S's class-extends-clause, then S is a subclass of T and T is a superclass of S; we also say that S inherits from T. This relationship also makes S a subtype of T, meaning that variables of type T can refer to objects of type S. In Java, when S is a subclass of T, then S inherits all the instance fields and methods from T.
A class may also implement several interfaces, declared in its implements-clause; the class thus becomes a subtype of each of the interfaces that it implements.
Similarly, an interface may extend several other interfaces. In Java, such an interface inherits all of the abstract methods and static final fields from the interfaces it extends. When interface U extends another interface V, then U is a subtype of V.
In addition, every type in Java is a subtype of Object.
In particular every class S and every interface U is
a subtype of Object.
In JML, model and ghost features, as well as specifications are inherited. A subtype inherits from its supertypes:
It is an error for a type to inherit a field x from two different supertypes if that field is declared with different types.
It is an error for a type to inherit a method with the same formal parameter types but with either different return types or with conflicting throws clauses [Gosling-etal00].
In Java one cannot inherit method implementations from interfaces, but this is possible in JML, where one can implement a model method in an interface. It is illegal for a class or interface to inherit two different implementations of a model method.
In JML, specifications of supertypes are inherited by subtypes, and thus must be obeyed by subtypes. This forces subtypes to be behavioral subtypes [Dhara-Leavens96] [Leavens-Naumann06] [Leavens06b]. See section 11. Specification Inheritance, for details about specification inheritance and behavioral subtyping.
In addition to the Java modifiers that can be legally attached to a class or interface declaration [Gosling-etal00], in JML one can use the following modifiers.
pure model spec_java_math spec_safe_math spec_bigint_math code_java_math code_safe_math code_bigint_math nullable_by_default |
The modifiers spec_java_math, spec_safe_math,
and spec_bigint_math are mutually exclusive.
They declare that all the math used in the type's
specifications uses the rules of Java's math, safe math, or bigint
math, respectively.
The modifiers code_java_math, code_safe_math,
and code_bigint_math are also mutually exclusive.
They say that the math used in the type's Java
code uses the rules of Java's math, safe math, or bigint
math, respectively.
See section 6.2.12 Math Modifiers, for more details on these modifiers.
We discuss the use of pure and model on type
declarations below.
6.1.2.1 Pure Type Declarations 6.1.2.2 Model Type Declarations
A type declaration may be modified with the JML modifier keyword pure.
The effect of declaring a type pure is that all constructor and
instance method declarations within the type are automatically
declared to be pure
(see section 7.1.1.3 Pure Methods and Constructors, for more about pure methods).
However, its static methods may still have side effects in a type
declared with pure,
as the pure does not apply to the static methods
declared in a type. So, in essence, declaring a class pure
is merely a shorthand for declaring all of the constructors and
instance methods declared in that class pure.
Although an override of a pure method must be pure, instance methods declared in subtypes that do not override a pure supertype's methods need not be pure. Hence, some methods of such a subtype object may mutate the objects of such a subtype. In other words, such a subtype does not necessarily have immutable objects.
However, if one is careful, once an object of class declared to be
pure is created,
such an object will be immutable, since
none of its instance methods will have any side effects.
Being careful to avoid problems means first that the class's fields
must be either final or encapsulated
(e.g., declared as private, to avoid direct mutation by clients),
and second that the type's constructors and methods,
must either avoid representation exposure
(see section 18.1 Basic Concepts of Universes)
or all of its fields must be immutable objects or values (such as integers).
A type declaration that is declared with the modifier model
is a specification-only type.
Hence, such a type may not be used in Java code, and may only be used
in annotations. It follows that the
entire type declaration must be contained within an annotation comment,
and consequently annotations within the type declaration do not need to
be separately enclosed in annotation comments.
The scope rules for a model type declaration are the same as for Java type definitions, except that a model type declaration is not in scope for any Java code, only for annotations.
Types declared with the keyword model are seldom used in JML.
If a tool does not support such types, one can always just define a
Java type, which will also be useful in runtime assertion checking.
Various authors refer to "model types" when they really mean "types
with modifier pure that are used for modeling."
Such a usage is contrary to JML's notion of a type with a model
modifier.
The following is the syntax of modifiers.
modifiers ::= [ modifier ] ... modifier ::= |
The jml-modifiers are only recognized as keywords in annotation comments. See section 4. Lexical Conventions, for more details.
The Java modifiers have the same meaning as in Java [Gosling-etal00].
Note that although the modifiers grammar non-terminal is used in many places throughout the grammar, not all modifiers can be used with every grammar construct. See the discussion regarding each grammar construct, which is summarized in D. Modifier Summary.
In the following we first discuss the suggested ordering of modifiers The rest of this section discusses the JML-specific modifiers in general terms. Their use and meaning for each kind of grammatical construct should be consulted directly for more details.
There are various guidelines for ordering modifiers in Java (see, for example section 8 of [Gosling-etal00], which is enforced by Checkstyle). As JML has several extra modifiers, we also suggest an ordering; although this ordering is not enforced, various tools may give warnings if the suggestions are not followed, as following a standard ordering tends to make reading declarations easier. For use in JML, we suggest the following ordering groups, where the ones at the top should appear first (leftmost), and the ones at the bottom should appear last (rightmost). In each line, the modifiers are either mutually exclusive, or their order does not matter (or both).
java-annotations public private protected spec_public spec_protected abstract static model ghost pure final synchronized instance transient volatile native strictfp monitored uninitialized helper spec_java_math spec_safe_math spec_bigint_math code_java_math code_safe_math code_bigint_math non_null nullable nullable_by_default code extract peer rep readonly |
A Java annotation (see section 9.7 of [Gosling-etal05]) has the following syntax. Note that these are quite different from JML annotations (see section 4.4 Annotation Markers).
java-annotations ::= java-annotation [ java-annotation ] ... java-annotation ::= |
A Java annotation forms part of the Java interface of a declaration, and as such is only satisfied by an implementation if the implementation contains the same annotation. Its semantics and checking is exactly as in Java.
The spec_public modifier allows one to declare a feature as public
for specification purposes. It can only be used when the feature has
a more restrictive visibility in Java. A spec_public field is
also implicitly a data group.
The spec_protected modifier allows one to declare a feature as protected
for specification purposes. It can only be used when the feature has
a more restrictive visibility in Java. That is, it can only be used
to change the visibility of a field or method that is, for Java,
either declared private or default access (package visible).
A spec_protected field is
also implicitly a data group.
In general terms, a pure feature is one that has no side effects when
executed. In essence pure only applies to methods and
constructors. The use of pure for a type declaration is
shorthand for applying that modifier to all constructors and instance
methods in the type (see section 6.1.2 Modifiers for Type Declarations).
See section 7.1.1.3 Pure Methods and Constructors, for the exact semantics of pure methods and constructors.
The model modifier introduces a specification-only feature. For
fields it also has a special meaning, which is that the field can be
represented by concrete fields. See section 2.2 Model and Ghost.
The modifiers model and ghost are mutually exclusive.
A model field may not be declared to be final. This is
because model fields are abstractions of concrete fields,
and thus it would complicate JML to allow final model fields.
If you feel that you want a final model field, what you should use
instead is a final ghost field. See section 6.2.7 Ghost.
Note that in an interface, a model field is implicitly declared
to be static. Thus if you want an instance field, you should use the
modifier instance, so that the field will act as if it were a
member of all objects whose type is a subtype of that interface.
Conversely, in a class, a model field is implicitly declared to be
instance. Thus, if you want a static field, you should use the
modifier static, so that the value of the model field is
shared by all instances of the class and its subclasses.
The ghost modifier introduces a specification-only field that
is maintained by special set statements. See section 2.2 Model and Ghost.
The modifiers ghost and model are mutually exclusive.
A ghost field declared in an interface is not final by
default. If you want a final ghost field in an interface, you
must declare it to be final explicitly. Ghost fields in
classes are also not final by default.
In an interface, a ghost field is implicitly declared
to be static. Thus if you want an instance field, you should use the
modifier instance, so that the field will act as if it were a
member of all objects whose type is a subtype of that interface.
Conversely, in a class, a ghost field is implicitly declared to be
instance. Thus, if you want a static field, you should use the
modifier static, so that the value of the ghost field is
shared by all instances of the class and its subclasses.
The instance modifier says that a field is not static.
See section 2.5 Instance vs. Static.
The helper modifier may be used on a method that is either pure
or private or on a private constructor to say that its
specification is not augmented by invariants and history constraints
that would otherwise be relevant.
that is, when a method or constructor is declared with the
helper modifier, no invariants or history constraints apply to it
(see section 7.1.1.4 Helper Methods and Constructors).
Thus helper makes such a method or constructor an exception to the
general rule that each invariant must be obeyed
by all methods in a class or interface and its subtypes.
(see section 8.2 Invariants).
Similar remarks apply to helper methods and history constraints.
The paper "Information Hiding and Visibility in Interface
Specifications" [Leavens-Mueller07]
describes why helper methods must be private.
Essentially, the reason is that a helper method (or constructor) may
violate various invariants, and all of the potentially violated
invariants "must be visible wherever the helper method is visible"
(Rule 7 in Section 5.2 of [Leavens-Mueller07]).
The only way to guarantee that in all cases all such invariants are
visible is to force all helper methods to be private.
However, the discussion in that paper did not consider pure methods,
and it is sometimes helpful to make a pure method a helper method, so
this case is also allowed.
The monitored modifier may be used on a non-model field
declaration to say that a thread must hold the lock on the object that
contains the field (i.e., the this object containing the field)
before it may read or write the field [Leino-Nelson-Saxe00].
The uninitialized modifier may be used on a field
declaration to say that despite the initializer, the location declared
is to be considered uninitialized. Thus, the field should
be assigned in each path before it is read.
[Leino-Nelson-Saxe00].
The modifiers
spec_java_math,
spec_safe_math,
spec_bigint_math,
code_java_math,
code_safe_math, and
code_bigint_math
describe what math modes are used for specifications
(spec_...) and for Java code (code_...)
[Chalin04].
For each of these two dimensions of specifications and code,
there are there are three kinds of math modes.
1+Integer.MAX_VALUE
will equal 1+Integer.MIN_VALUE.
This is the default math mode.
1+Integer.MAX_VALUE will throw an exception.
1+Integer.MAX_VALUE will be the next integer past
Integer.MAX_VALUE.
The spec_ modifiers spec_java_math, spec_safe_math,
and spec_bigint_math determine the kind of mathematics used in
specifications at the level in which the modifier appears.
For example, if the modifier spec_java_math is used on a type
declaration, all arithmetic used in specifications written in
that type use Java math mode.
Similarly, if the modifier spec_java_math is used on a method
declaration, then Java math mode will be used for the
specifications written in that file for that method.
The mode spec_java_math is the default math used in
specifications, used if neither spec_safe_math,
nor spec_bigint_math are given. Within a type marked with one
of these modifiers, individual method or constructors can have one of
the other modifiers, which is used for that method or constructor's
specifications in that file.
Similarly, spec_safe_math specifies that safe math mode will be
used for the specifications in the type or method to which it is
attached,
and spec_bigint_math specifies that bigint math mode will be
used for the specifications in the type or method to which it is
attached.
The modifiers code_java_math, code_safe_math,
and code_bigint_math are similar to the specification math
modes, but describe the way that the Java code used in an
implementation is compiled.
For example, code_java_math specifies that the type or method
to which the modifier is attached is to be compiled using the default Java
math mode.
For example, code_safe_math specifies that the type or method
to which the modifier is attached is to be compiled using the safe
math mode,
and code_bigint_math specifies that the type or method
to which the modifier is attached is to be compiled using bigint
math mode.
These modes are level 2 features of JML. See Chalin's paper [Chalin04] for more details on the use of these modes.
Any declaration (other than that of a local variable)
whose type is a reference type
is implicitly declared non_null unless (explicitly or implicitly)
declared nullable. Hence reference type declarations are
assumed to be non-null by default (see section 2.8 Null is Not the Default).
A declaration can be explicitly declared nullable by annotating
it with the nullable modifier.
A declaration is implicitly declared nullable when the (outer
most) class or interface containing the declaration is adorned by the
class-level modifier nullable_by_default.
Attempting to use both the non_null and nullable
modifiers is a compile time error.
| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |