Open AccessStatic Correctness of Hierarchical Procedures
Author(s) -
Michael I. Schwartzbach
Publication year - 1989
Publication title -
daimi pb
Language(s) - English
Resource type - Journals
eISSN - 2245-9316
pISSN - 0105-8517
DOI - 10.7146/dpb.v18i295.6689
Subject(s) - correctness , hierarchy , computer science , exploit , type (biology) , programming language , theoretical computer science , inheritance (genetic algorithm) , property (philosophy) , algorithm , ecology , biochemistry , chemistry , philosophy , computer security , epistemology , economics , gene , market economy , biology
A system of hierarchical, imperative, fully recursive types allows program fragments written for small types to be reused for all larger types. To exploit this property to enable type-safe hierarchical procedures, it is necessary to impose a static requirement on procedure calls. We introduce an example language and prove the existence of a sound requirement which preserves static correctness while allowing hierarchical procedures. This requirement is further shown to be optimal , in the sense that it imposes as few restrictions as possible. This establishes the theoretical basis for a very powerful and general type hierarchy with static type checking, which enables 1st order polymorphism and (multiple) inheritance in a language with assignments.