3.9 Type Checking Predicate Objects

Predicate objects are intended to represent alternative ways of implementing an object's interface. Accordingly, it should be possible to type-check programs using predicate objects, under the assumption that the particular state of the object does not affect its external interface. In particular, to guarantee type safety in the presence of predicate objects, the type checker must verify that for each message declared in the interface of some object O:

• at all times there is an implementation of the message inherited by the object O; and
• at no time are there several mutually ambiguous implementations of the message inherited by the object O.

These two tests correspond to extending the tests of completeness and consistency of method implementations to cope with the presence of predicate objects.

The set of methods inherited by the object O from normal objects is fixed at program-definition time and can be type-checked in the standard way. Methods inherited from predicate objects pose more of a problem. If two predicate objects might be inherited simultaneously by an object, either one predicate object must be known to override the other or they must have disjoint method names. For example, in the bounded buffer implementation described in section 2.4, since an object can inherit from both the non_empty_buffer and the non_full_buffer predicate objects, the two predicate objects should not implement methods with the same name. Similarly, if the only implementations of some message are in some set of predicate objects, then one of the predicate objects must always be inherited for the message to be guaranteed to be understood. In other words, the checker needs to know when one predicate object implies another, when two predicate objects are mutually exclusive, and when a group of predicate objects is exhaustive. Once these relationships among predicate objects are determined, the rest of type-checking becomes straightforward.

Ideally, the system would be able to determine all these relationships automatically by examining the predicate expressions attached to the various predicate objects. However, predicate expressions in Cecil can run arbitrary user-defined code, and consequently the system would have a hard time automatically inferring implication, mutual exclusion, and exhaustiveness. Consequently, we rely on explicit user declarations to determine the relationships among predicate objects; the system can verify dynamically that these declarations are correct.

A declaration already exists to describe when one predicate object implies another: the isa declaration. If one predicate object explicitly inherits from another, then the first object's predicate is assumed to imply the second object's predicate. Any methods in the child predicate object override those in the ancestor, resolving any ambiguities between them.

Mutual exclusion and exhaustiveness are specified using declarations of the following form:

disjoint_decl	::=	"disjoint" named_objects ";"
cover_decl	::=	"cover" named_object "by" named_objects ";"
divide_decl	::=	"divide" named_object "into" named_objects ";"
named_objects	::=	named_object { "," named_object }

The disjoint declaration

disjoint object1, ..., objectn;

implies to the static type checker that the predicate objects named by each of the object_i will never be inherited simultaneously, i.e., that at most one of their predicate expressions will evaluate to true at any given time. Mutual exclusion of two predicate objects implies that the type checker should not be concerned if both predicate objects define methods with the same name, since they cannot both be inherited by an object. To illustrate, the following declarations extend the earlier bounded buffer example with mutual exclusion information:

disjoint empty_buffer, non_empty_buffer;
disjoint full_buffer, non_full_buffer;

The system can infer that empty_buffer and full_buffer are mutually exclusive with partially_full_buffer. Note that empty_buffer and full_buffer are not necessarily mutually exclusive.

The cover declaration

cover object by object1, ..., objectn;

implies that whenever an object O descends from object, the object O will also descend from at least one of the object_i predicate objects; each of the object_i are expected to descend from object already. Exhaustiveness implies that if all of the object_i implement some message, then any object inheriting from object will understand the message. For example, the following coverage declaration extends the bounded buffer predicate objects:

cover buffer by empty_buffer, partially_full_buffer, full_buffer;

Often a group of predicate objects divide an abstraction into a set of exhaustive, mutually-exclusive subcases. The divide syntactic sugar makes specifying such situations easier. A declaration of the form

divide object into object1, ..., objectn;

is syntactic sugar for the following two declarations:

disjoint object1, ..., objectn;
cover object by object1, ..., objectn;

Since fields are accessed solely through accessor methods, checking accesses to fields in predicate objects reduces to checking legality of messages in the presence of predicate objects, as described above. To ensure that fields are always initialized before being accessed, the type checker simply checks that the values of all fields potentially inherited by an object are initialized either at the declaration of the field or at the creation of the object.