3 Static Types
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 objecti 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:
The system can infer thatdisjoint
empty_buffer, non_empty_buffer;disjoint
full_buffer, non_full_buffer;
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
implies that whenever an object O descends from object, the object O will also descend from at least one of the objecti predicate objects; each of the objecti are expected to descend from object already. Exhaustiveness implies that if all of the objecti 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
objectby
object1, ..., objectn;
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 formcover
bufferby
empty_buffer, partially_full_buffer, full_buffer;
is syntactic sugar for the following two declarations:divide
objectinto
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.disjoint object1
, ..., objectn;cover
objectby
object1, ..., objectn;
Generated with Harlequin WebMaker