[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

7. Class and Interface Member Declarations

The nonterminal field describes all the members of classes and interfaces (see section 6.1 Class and Interface Declarations).

 
field ::= member-decl
        | jml-declaration
        | class-initializer-decl
        | ;

Also see section G.2.1 Non-null by Default. In the rest of this chapter we describe mostly the syntax and Java details of member declarations and class initializers. See section 8. Type Specifications, for the syntax and semantics of jml-declaration, and, more generally, how to use JML to specify the behavior of types.

7.1 Java Member Declarations  
7.2 Class Initializer Declarations  


7.1 Java Member Declarations

The following gives the syntax of Java member declarations.

 
member-decl ::= method-decl
        | variable-definition
        | class-declaration
        | interface-declaration

See section 6.1 Class and Interface Declarations, for details of class-declaration and interface-declaration. We discuss method and variable declarations below.

7.1.1 Method and Constructor Declarations  
7.1.2 Field and Variable Declarations  


7.1.1 Method and Constructor Declarations

The following is the syntax of a method declaration.

 
method-decl ::= [ doc-comment ] ...
                method-specification
                modifiers [ method-or-constructor-keyword ]
                [ type-spec ] method-head
                method-body
        | [ doc-comment ] ...
          modifiers [ method-or-constructor-keyword ]
          [ type-spec ] method-head
          [ method-specification ]
          method-body
method-or-constructor-keyword ::= method | constructor
method-head ::= ident formals [ dims ] [ throws-clause ]
method-body ::= compound-statement | ;
throws-clause ::= throws name [ , name ] ...

Notice that the specification of a method (see section 9. Method Specifications) may appear either before or after the method-head.

The use of non_null as a modifier in a method-decl really is shorthand for a postcondition describing the normal result of a method, indicating that it must not be null. It can also be seen as a modifier on the method's result type, saying that the type returned does not contain null.

The use of extract as a modifier in a method-decl is shorthand for writing a model program specification. See section 15.2 Extracting Model Program Specifications, for an explanation of this modifier.

7.1.1.1 Formal Parameters  
7.1.1.2 Model Methods and Constructors  
7.1.1.3 Pure Methods and Constructors  
7.1.1.4 Helper Methods and Constructors  


7.1.1.1 Formal Parameters

 
formals ::= ( [ param-declaration-list ] )
param-declaration-list ::= param-declaration
                           [ , param-declaration ] ...
param-declaration ::= [ param-modifier ] ... type-spec ident [ dims ]

param-modifier ::= final | non_null | nullable

See section 7.1.2.2 Type-Specs, for more about the nonterminals type-spec and dims.

The modifier non_null when attached to a formal parameter is shorthand for a precondition that says that the corresponding actual parameter may not be null. The type of a parameter that has the non_null modifier must be a reference type [Raghavan-Leavens05].

The non_null modifier on a parameter is inherited in the same way as the equivalent precondition would be, so it need not be declared on every declaration of the same method in a subtype or refinement. The non_null modifier may be added to a method in a separate file (see section 17. Separate Files for Specifications), and thus need not appear originally in the Java source code. It can be added to a method override in a subtype, but that will generally make the method non-implementable, as the method must also satisfy an inherited specification without the corresponding precondition.


7.1.1.2 Model Methods and Constructors

A method or constructor that uses the modifier model is called a model method or constructor. Since a model method is not visible to Java code, the entire method, including its body, should be written in an annotation.

As usual in JML (see section 2.2 Model and Ghost), a model method or constructor is a specification-only feature. A model method or constructor may have either a body or a specification, or both. The specification may be used in various verification tools, while the body allows it to be executed during runtime assertion checking. Model methods may also be abstract, and both model methods and constructors may be final (although there is no particular purpose served by making a constructor final, since constructors are not overridden in any case).

It is usual in JML to declare model methods and constructors as pure. However, it is possible to have a model method or constructor that is not pure; such methods are useful in model programs (see section 15. Model Programs). On the other hand, aside from their use in model programs, most model methods only exist to be called in assertions, and since only pure methods can be called in assertions, they should usually be declared as pure.


7.1.1.3 Pure Methods and Constructors

This subsubsection, which describes the effect of the pure modifier on methods and constructor declarations, is quoted from the preliminary design document [Leavens-Baker-Ruby06].

We say a method is pure if it is either specified with the modifier pure or is a method that appears in the specification of a pure interface or class. Similarly, a constructor is pure if it is either specified with the modifier pure or appears in the specification of a pure class.

A pure method that is not a constructor implicitly has a specification that does not allow any side-effects. That is, its specification has the clauses
 
           diverges false;
           assignable \nothing;
added to each specification case; if the method has no specification given explicitly, then these clauses are added as a lightweight specification. For this reason, if one is writing a pure method, it is not necessary to otherwise specify an assignable clause (see section 9.9.9 Assignable Clauses), although doing so may improve the specification's clarity.

A pure constructor has the clauses
 
           diverges false;
           assignable this.*;
added to each specification case; if the constructor has no specification given explicitly, then these clauses are added as a lightweight specification. This specification allows the constructor to assign to the non-static fields of the class in which it appears (including those inherited from its superclasses and ghost model instance fields from the interfaces that it implements).

Implementations of pure methods and constructors will be checked to see that they meet these conditions on what locations they can assign to. To make such checking modular, some JML tools prohibit a pure method or constructor implementation from calling methods or constructors that are not pure. However, more sophisticated tools could more directly check the intended semantics [Salcianu-Rinard05].

A pure method or constructor must also be provably terminating. Although JML does not force users to make such proofs of termination, users writing pure methods and constructors are supposed to make pure methods total in the sense that whenever, a pure method is called it either returns normally or throws some exception. This is supposed to lessen the possibility that assertion evaluation could loop forever, aids theorem provers by making pure methods more like mathematical functions.

Furthermore, a pure method is supposed to always either terminate normally or throw an exception, even for calls that do not satisfy its precondition. Static verification tools for JML should enforce this condition, by requiring a proof that a pure method implementation satisfies the following specification
 
   private behavior
     requires true;
     diverges false;
     assignable \nothing;
(and similarly for constructors, except that the assignable clause becomes assignable this.*; for constructors).

However, this implicit verification condition is a specification, and thus cannot be used in reasoning about calls to the method, even calls from within the class itself and recursive calls from within the implementation. For this reason we recommend writing the method or constructor specification in such a way that the effective precondition of the method is "true," making the proof of the above implicit verification condition trivial, and allowing the termination behavior of the implementation to be relied upon by all clients.

Recursion is permitted, both in the implementation of pure methods and the data structures they manipulate, and in the specifications of pure methods. When recursion is used in a specification, the proof of well-formedness for the specification involves the use of JML's measured_by clause.

Since a pure method may not go into an infinite loop, if it has a non-trivial precondition, it should throw an exception when its normal precondition is not met. This exceptional behavior does not have to be specified or programmed explicitly, but technically there is an obligation to meet the specification that the method never loops forever.

Furthermore, a pure method must be deterministic, in the sense that when called in a given state, it must always return the same value. Similarly a pure constructor should be deterministic in the sense that when called in a given state, it always initializes the object in the same way.

A pure method can be declared in any class or interface, and a pure constructor can be declared in any class. JML will specify the pure methods and constructors in the standard Java libraries as pure.

As a convenience, instead of writing pure on each method declared in a class and interface, one can use the modifier pure on classes and interfaces and classes. This simply means that each non-static method and each constructor declared in such a class or interface is pure. Note that this does not mean that all methods inherited (but not declared in and hence not overridden in) the class or interface are pure. For example, every class inherits ultimately from java.lang.Object, which has some methods, such as notify and notifyAll that are manifestly not pure. Thus each class will have some methods that are not pure. Despite this, it is convenient to refer to classes and interfaces declared with the pure modifier as pure.

In JML the modifiers model and pure are orthogonal. (Recall something declared with the modifier model does not have to be implemented, and is used purely for specification purposes.) Therefore, one can have a model method that is not pure (these might be useful in JML's model programs) and a pure method that is not a model method. Nevertheless, usually a model method (or constructor) should be pure, since there is no way to use non-pure methods in an assertion, and model methods cannot be used in normal Java code.

By the same reasoning, model classes should, in general, also be pure. Model classes cannot be used in normal Java code, and hence their methods are only useful in assertions (and JML's model programs). Hence it is typical, although not required, that a model class also be a pure class.

As can be seen from the semantics, if a pure method has a return type of void, then it can essentially only do nothing. So, while pure methods with void as their return type are not illegal, they are useless.


7.1.1.4 Helper Methods and Constructors

The helper modifier may only be used on a private method or constructor [Leavens-Mueller07]. See section 6.2.9 Helper, for more on why such methods and constructors must be private.

A method or constructor with the helper modifier, has a specification that is not augmented by invariants and history constraints that would otherwise apply to it. It can thus be thought of as an abbreviation device. However, whatever specifications are given explicitly for such a method or constructor still apply. See section 8.2 Invariants, for more details.


7.1.2 Field and Variable Declarations

The following is the syntax of field and variable declarations.

 
variable-definition ::= [ doc-comment ] ... modifiers variable-decls
variable-decls ::= [ field ] type-spec variable-declarators ;
                   [ jml-data-group-clause ] ...
variable-declarators ::= variable-declarator
                         [ , variable-declarator ] ...
variable-declarator ::= ident [ dims ] [ = initializer ]
initializer ::= expression | array-initializer
array-initializer ::= { [ initializer-list ] } 
initializer-list ::= initializer [ , initializer ] ... [ , ]

The field keyword is not normally needed, but can be used to change JML's parsing mode. Within an annotation, such as within a declaration of a model method, it is sometimes necessary to switch from JML annotation mode to JML spec-expression mode, in order to parse words that are JML keywords but should be recognized as Java identifiers. This can be accomplished in a field declaration by using the keyword field, which changes parsing to spec-expression mode. [[[ When does the mode revert back? e.g. in a method declaration - DRC]]]

[[[Needs example, move elsewhere?]]]

In a non-Java file, such as a file with suffix `.jml' (see section 17. Separate Files for Specifications), one may omit the initializer of a variable-declarator, even one declared to be final. In such a file, one may also omit the body of a method-decl. Of course, in a `.java' file, one must obey all the rules of Java for declarations that are not in annotations.

See section 10. Data Groups, for more about jml-data-group-clauses. See section 12.2 Specification Expressions, for the syntax of expression. In the following we discuss the modifiers for field and variable declarations and type-specs.

7.1.2.1 JML Modifiers for Fields  
7.1.2.2 Type-Specs  


7.1.2.1 JML Modifiers for Fields

The ghost and model modifiers for fields both say that the field is a specification-only field; it thus cannot be accessed by the Java code. The difference is that a ghost field is explicitly manipulated by initializations and set statements (see section 13. Statements and Annotation Statements), whereas a model field cannot be explicitly manipulated. Instead a model field is indirectly given a value by a represents clause (see section 8.4 Represents Clauses). See section 2.2 Model and Ghost, for a general discussion of this distinction in JML.

While fields can be declared as either model or ghost fields, a field cannot be both. Furthermore, local variables cannot be declared with the model modifier.

The non_null modifier in a variable declaration is shorthand for an invariant saying that each variable declared in the variable-decls may not be null. This invariant has the same visibility as the visibility declaration of the variable-definition itself. See section 8.2 Invariants, for more about invariants.

The monitored modifier says that each variable declared in the variable-decls can only be accessed by a thread that holds the lock on the object that contains the field [Leino-Nelson-Saxe00]. It may not be used with model fields.

The instance modifier says that the field is to be found in instances instead of in class objects; it is the opposite of static. It is typically only needed for model or ghost fields declared in interfaces. When used in an interface, it makes the field both non-static and non-final (unless the final modifier is used explicitly). See section 2.5 Instance vs. Static.

To declare a static field in an interface, one omits the instance modifier; such a field, as in Java is both static and final.


7.1.2.2 Type-Specs

The syntax of a type-spec is as in Java [Gosling-etal00], except for the addition of the type \TYPE and the possibility of using ownership-modifiers. The ownership-modifiers are only available when the Universe type system is turned on. See section 18. Universe Type System, for how to do that, and for the syntax and semantics of ownership-modifiers.

 
type-spec ::= [ ownership-modifiers ] type [ dims ]
         | \TYPE [ dims ]
type ::= reference-type | built-in-type
reference-type ::= name
dims ::= `[' `]' [ `[' `]' ] ...

The type \TYPE represents the kind of all Java types. It can only be used in annotations. It is equivalent to java.lang.Class.


7.2 Class Initializer Declarations

The following is the syntax of class initializers.

 
class-initializer-decl ::= [ method-specification ]
                           [ static ] compound-statement
        | method-specification static_initializer 
        | method-specification initializer 

The first form above is the form of Java class instance and static initializers. The initializer is static, and thus run when the class is loaded, if it is labeled static. The effect of the initializer can be specified by a JML method specification (see section 9. Method Specifications), which treats the initializer as a private helper method with return type void, whose body is given by the compound-statement (see section 13. Statements and Annotation Statements).

The last two forms are used in JML to specify static and instance initializers without giving the body of the initializer. They would be used in annotations in non-Java files (see section 17. Separate Files for Specifications). At most one of each of these may appear in a type specification file. Such a specification is satisfied if there is at least one corresponding initializer in the implementation, and if the sequential composition of the bodies of the corresponding initializer(s), when considered as the body of a private helper method with return type void, satisfy the specification given (see section 9. Method Specifications).

Note that, due to this semantics, the method-specifications for an initializer can only have private specification cases.

[[[ But initializers can be interspersed between field initializations, which will affect their meaning. Thus I think the composition has to include the field initializations. The effect is that the post-condition of the JML initializer refers to the state before a constructor begins executing; a static_initializer refers to the state after class loading, I think. -- DRCok ]]] [[[ Is the restriction to private true for static initialization as well - don't think it should be. - DRCOk ]]]


[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

This document was generated by U-leavens-nd\leavens on May, 31 2013 using texi2html