Abstract formal framework for method overriding

Abstract

Automated verification on method overriding is important in Object- Oriented Programming Language (OOPL) to reduce human errors during software verification process. Static verification method fails to address the issue effectively. This paper examines the issues in developing semantics for verifying method overriding in OOPL. The purpose is to identify elements or components for verification process. A study conducted on literature reveals two main issues of verifying method overriding: subtyping and class invariant. Both issues are resolvable by integrating the elements of non-reverification, modularity, and programmer intervention into a framework. We propose an abstract formal framework with the integration of the three elements by using abstract interpretation and Lazy Behavioral Subtyping (LBS). The framework shows that the integration of less restriction of LBS and abstract interpretation is possible to achieve automated verification. © 2011 Springer-Verlag.