16. Specification for Subtypes

This chapter describes how JML specifies a type so that one can program subtypes from the specification, without the need to see the code of the supertypes that have been specified.

The problem of specifying enough about superclasses has been discussed by Kiczales and Lamping [Kiczales-Lamping92] and by Steyaert, et al. [Steyaert-etal96]. This problem is difficult because of the many ways that subclasses can depend on coding details of a superclass. For example, a subclass can depend on the calling pattern among a superclass's method and the fields that a superclass can access [Kiczales-Lamping92] [Steyaert-etal96].

JML builds on the work of Ruby and Leavens to solve this problem [Ruby-Leavens00] [Ruby06], which builds on the earlier works described above. The idea is to write specifications for subclasses in three parts. The first is the usual, public specification, which is primarily for clients but also useful to subclasses, who need to know what public interface they must meet. The second is a protected specification, which specifies fields and methods that are usable by the subclass. The third is the code contract. The code contract has a different syntax in JML than it did in [Ruby-Leavens00]. In the current JML a code contract is a heavyweight behavior specification case (see section 9.5 Heavyweight Specification Cases) or as a model program (see section 15. Model Programs) that uses the keyword "code." The code keyword is used just before one of the behavior keywords or just before the keyword model_program.

While code contracts can be generated automatically by a tool, as imagined by Ruby and Leavens [Ruby-Leavens00] [Ruby06], they can also be written by users directly. This is sometimes useful for documenting the implementation of a method. The code contract is intended to be created automatically, by a tool (which does not, as of this writing, exist). It has the following syntax.

In code contracts as described in the work of Ruby and Leavens, the main clauses used are the accessible-clause and the callable-clause. See section 9.9.10 Accessible Clauses, for the syntax and semantics of the accessible-clause. See section 9.9.11 Callable Clauses, for the syntax and semantics of the callable-clause.

16.1 Method of Specifying for Subclasses
16.2 Code Contracts

16.1 Method of Specifying for Subclasses

[[[This should be a synopsis of Clyde Ruby's dissertation, with an example.]]]

16.2 Code Contracts

This section discusses the semantics of "code contracts," which are specification cases that use the "code" keyword. (See section 9.6 Behavior Specification Cases, for the detailed syntax of such specification cases.)

This feature was inspired by "does" clause of the Alloy Annotation Language [Khurshid-Marinov-Jackson02].

The modifier code may not be used on an abstract method. It follows that the code modifier cannot be used to document normal Java methods in interfaces. (In an interface, code could only be used in the specification of a model method that has a body.)

Tools for JML should warn the user if code is used in a specification case for a constructor, or for a final, static, or private method. It does no harm there, but is not needed.

The meaning of the code modifier is just that specification cases or model programs containing them are not inherited. That is, whenever the method is overridden, it does not inherit code contracts from its supertypes.

In verification of a method call, you can use all non-code specification cases, that are visible at a call site, for the statically-determined method being called. Such specifications are inherited by each subtype's method overrides to preserve behavioral subtyping [Dhara-Leavens96] [Leavens-Naumann06] [Leavens06b].

In verification of a method call, you can use a code specification case for a method m given in a class C only if you can prove that the method being called is method m in class C. This applies in particular to super calls, which is the main use for such code contracts. (It would also apply to calls to final methods, calls to methods in final classes, and calls to private or static methods.)