Invariants generation for method overriding using abstract interpretation / Siti Hafizah Ab. Hamid

Software verification is an important element of software reliability. The significance and importance of verification have been recognized by Bill Gates in his speech in WinHEC 2002. The software verification allows program’s specification to be formally proved to ensure the specification verified the program before its execution time using static analysis. However, in the context of object-oriented program, studies show there is a need to have formal specifications for method overriding because the overriding feature plays important role in allowing program reusability. This thesis develops an abstract formal framework for invariant generation of static analysis for method overriding in object-oriented program using inheritance. It focuses on late bound method in the class invariants generation. There are two main problems arise during the process of generating class invariant which are reverification of class invariant and over-approximation of late binding call. In the context of method overriding, the problem of late binding call happens when the abstract semantic function uses behavioral subtyping that is restricted to the rule of contravariance and covariance. The abstract formal framework using abstract interpretation theory is proposed to overcome the problem above. The framework exploits the capability of abstract interpretation method in making program analysis automated. It also overcomes the problem of generating the invariants for late binding call of method overriding with less restrictions rules of lazy behavioral subtyping method. The use of lazy behavioral subtyping results to the overridden method semantics has a not over approximated invariant. The framework produces two equations for two invariants, which are modular invariants for inheritance and invariants for method overriding. A scenario based evaluation is conducted to validate the invariants and to compare the proposed framework using lazy behavioral subtyping with the framework using behavioral subtyping