STATIC CORRECTNESS OF HIERARCHICAL PROCEDURES

A system of hierarchical, fully recursive types in a truly imperative language allows program fragments written for small types to be reused for all larger types. To exploit this property to enable type-safe hi erarchical procedures, it is necessary to impose a static requirement on procedure calls. We introduce an example language and prove the exi stence of a sound requirement which preserves static correctness while allowing hierarchical procedures. This requirement is further shown t o be optimal, in the sense that it imposes as few restrictions as poss ible. This establishes the theoretical basis for a general type hierar chy with static type checking, which enables first-order polymorphism combined with multiple inheritance and specialization in a language wi th assignments. We extend the results to include opaque types. An opaq ue version of a type is different from the original but has the same v alues and the same order relations to other types. The opaque types al low a more flexible polymorphism and provide the usual pragmatic advan tages of distinguishing between intended and unintended type equalitie s. Opaque types can be viewed as a compromise between synonym types an d abstract types.