  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.

Logic in Computer Science;Programming Languages