Verifying OO Programs by Linking Algebraic and Abstract Specifications

In this paper, we propose an approach for verifying the correctness of object-oriented (OO) programs with respect to the algebraic specifications. Compared to the functional specification that emphasizes on specifying what a single operation does, algebraic specification, which was proposed originally for specifying abstract data types, specifies what different operations of a class are related to each other. We first extend the algebraic specification of abstract data types to OO programs, and then prove the conformance of the implementation of programs to the algebraic specifications by taking functional specification as a bridge.