3.2 Code Inheritance and Genericity

   Recall from section 3.1.2 that we conceptually discern subtyping and code inheritance. I.e., we consider subtyping and inheritance as two different techniques although they may have the same syntax in the programming language.

A code inheritance concept designed to support verification is more than a technique to copy implementations. Specifications and correctness proofs can be inherited along with program code. Consider a method m of class C implemented in module M. If M is verified it is already showed that C::m preserves all invariants of M. Consider a module N with class D inheriting m. To verify D, it is no more necessary to prove that D::m preserves the invariants of M as this was already showed for C::m. Thus, verification effort can be reduced.

Like composition, subtyping, and code inheritance, current programming languages support parameterized classes (or templates) on a syntactical level only. We want to derive the correctness of an instantiation of a parameterized class from the class itself and the type parameter. I.e., the aim is to specify and verify the template in a way that correctness is preserved for all possible instantiations of the template. Thus, we require all possible actual type parameters to be behavioral subtypes of the formal parameter type. This asserts that all methods of the type parameter behave in the expected way.

Consider a generic list with a method sort. To verify sort, it is required for every actual type parameter to provide a method less. Again, it is not sufficient to check syntactically the presence of this method. Verification requires to semantically guarantee that less establishes an ordering relation on the objects of that type. I.e., all actual type parameters have to be behavioral subtypes of a class defining method less with appropriate specification.

In general, genericity is not even well understood on a syntactic level. A lot of work has to be done to study different forms of genericity (e.g., different forms of parameters, like types or methods), and to develop a semantical notion of this technique that goes far beyond textual copies.