Academic
Publications
Inheritance and Modularity in Specification and Verification of OO Programs

Inheritance and Modularity in Specification and Verification of OO Programs,10.1109/TASE.2011.28,Liu Yijing,Hong Ali,Qiu Zongyan

Inheritance and Modularity in Specification and Verification of OO Programs  
BibTex | RIS | RefWorks Download
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 called 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.
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.