archives

Inheritance and formal verification of software

Inheritance is an important technique for abstraction in object oriented software. Functional languages like Haskell have some form of inheritance of concepts as well (e.g. the class Eq).

Verification techniques should therefore take inheritance into account.

By looking further into the topic it becomes evident that inheritance is a good vehicle for program verification as well i.e. inheritance helps verification.

Abstract classes can make some assumptions and prove some other properties based on the assumptions and the defined functions within the absract class.

A descendant of the abstract concepts just needs to substantiate the assumptions and can inherit all the proved proved properties of the abstract concept.

This technique is described in the article "inheritance" and demonstrated with some examples like equality, partial order and total order.