Verification of Object-Oriented Programs: a Transformational Approach

TL;DR

This paper presents a transformational approach to verify object-oriented programs by converting them into recursive programs, enabling simpler assertional proofs and establishing soundness and completeness of the proof system.

Contribution

It introduces a syntax-directed transformation from object-oriented to recursive programs, facilitating verification and proof rule development.

Findings

Transformation simplifies verification process

Proof system is sound and relatively complete

Handles arrays, instance variables, aliasing, and recursive methods

Abstract

We show that verification of object-oriented programs by means of the assertional method can be achieved in a simple way by exploiting a syntax-directed transformation from object-oriented programs to recursive programs. This transformation suggests natural proofs rules and its correctness helps us to establish soundness and relative completeness of the proposed proof system. One of the difficulties is how to properly deal in the assertion language with the instance variables and aliasing. The discussed programming language supports arrays, instance variables, failures and recursive methods with parameters.