| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The following is the syntax of type definitions.
type-definition ::= class-definition
| interface-definition
| |
The specification of a type-definition is determined as follows.
If the type-definition consists only of a semicolon (;),
then the specification is empty. Otherwise the specification is that
of the class or interface definition. Such a specification must be
satisfied by the corresponding class or interface definition.
The rest of this chapter discusses class and interface definitions, as well as the syntax of modifiers.
6.1 Class and Interface Definitions 6.2 Modifiers
Class and interface definitions are quite similar, as interfaces may be seen as a special kind of class definition that only allows the declaration of abstract instance methods and final static fields (in the Java code [Gosling-etal00]). Their syntax is also similar.
class-definition ::= [ 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 Definitions 6.1.2 Modifiers for Type Definitions
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 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]. (There are other restrictions on method inheritance that apply when MultiJava is used [Clifton-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, instance methods have to obey the specifications of all
methods they override. This, together with the inheritance of
invariants and history constraints, forces subtypes to be behavioral subtypes
[Dhara-Leavens96] [Leavens-Naumann06] [Leavens06b].
However, history constraints are not inherited from supertypes whose
names are marked with weakly in the relevant clause.
Such subtypes are weak behavioral subtypes, and should only be
used in ways that do not permit cross-type aliasing [Dhara-Leavens94b]
[Dhara97].
See the report, "Desugaring JML Method Specifications" [Raghavan-Leavens05] for more about the details of specification inheritance in JML.
In addition to the Java modifiers that can be legally attached to a class or interface definition [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 |
A type definition 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).
Hence, once an object of a class is created, it
will be immutable, and furthermore, none of its instance methods will
have any side effects. However, its static methods may still have
side effects, as the pure does not apply to the static methods
declared in a type. Furthermore, although an override of a pure
method must be pure, instance methods declared in
subtypes that do not override this supertype's methods
need not be pure. Hence, such a subtype does not necessarily have
immutable objects. So, in essence, declaring a class pure
is merely a shorthand for declaring all of the constructors and
instance methods pure.
[[[ Pure does not make a class immutable either, since a method might return a reference to an internal representation which is then modified by some non-pure method in its class. Is it sufficient if all fields are also fields of pure types (recursively)? Then there are arrays. And also all fields would need to be private to have immutability. - DRC ]]]
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 definition must be contained within an annotation comment,
and consequently annotations within the type definition do not need to
be separately enclosed in annotation comments,
as is demonstrated in the example below.
The scope rules for a model type definition are the same as for Java type
definitions, except that a model type definition is not in scope for any
Java code, only for annotations.
[[[Model types are seldom used in JML. Since the runtime assertion checker doesn't work with them, I wonder if it would be best to get rid of them completely. You could always just define a Java type, which would be useful for runtime assertion checking.]]]
[[[ May a model type definition appear in more than one specification file of a refinement sequence, with any member declarations being combined together? I'd prefer that it only be allowed to appear once and be required to be completely defined in one spec file - easier for tools. -- DRCok ]]]
[[[Need to explain the math modifiers.]]]
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 B. 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 [[[citations?]]]. 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).
public private protected spec_public spec_protected abstract static model ghost pure final synchronized instance helper transient volatile native strictfp monitored uninitialized 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 |
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 definition is
shorthand for applying that modifier to all constructors and instance
methods in the type (see section 6.1.2 Modifiers for Type Definitions).
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.6 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 private method or
constructor to say that its
specification is not augmented by invariants and history constraints
that would otherwise be relevant. Normally, an invariant applies to
all methods in a class or interface. However, an exception is made
for methods and constructors declared with the helper modifier.
See section 8.2 Invariants. [[[ Just on private? or just on non-overridable
methods? or just on non-overridden methods? - DRC]]]
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].
[[[Need explanation of these.]]]
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] | [ ? ] |