Inheritance and Modularity in Specification and Verification of OO Programs

Specification and verification for object oriented (OO) programs remains a great challenge despite of decades´ efforts. To address the problem, we propose a novel specification and verification framework, which supports abstraction and offers modularity via a set of scope and inheritance rules, and a concept calledemph{specification predicate}. The framework covers the most important OO features like encapsulation, inheritance and polymorphism, while only one specification per method is necessary. It can successfully deal with inheritance, keep still modularity in verification, and avoid re-verification of the implementation. We show how the framework can be integrated into an OO language, and use examples to illustrate how the specification and verification can be carried out in our framework following the structures of OO programs in an abstract and modular way.