Automatic Verification of Inheritance (pp. 139-143)

Aleksandar Kupusinac, Dusan Malbaski
Implementation of inheritance in programming languages as they are does not impose any restrictions regarding the relation between the superclass and its subclass. This means that in principle it is almost possible to derive any class from any other. On the other hand, from the theoretical point of view the inheritance models a specialization relationship, meaning that logically the subclass must be a specialization of the superclass. Breaking this rule causes serious problems especially with polymorphic replacement. This fact is a motivation to introduce the concept of correct inheritance and to establish the appropriate conditions that must be satisfied by the subclass. In the present paper, we discuss such formal conditions and develop a formal recursive algorithm for automatic verification of inheritance. The solution is based solely on the first-order predicate logic.