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 novel specification framework, which supports abstraction offers modularity via set scope inheritance rules, concept called\emph{specification predicate}. The framework covers most important OO features like encapsulation, polymorphism, while only one per method is necessary. It can successfully deal with inheritance, keep still in verification, avoid re-verification implementation. We show how be integrated into an language, use examples to illustrate carried out our following structures abstract modular way.