Towards a Calculus of Object Programs

TL;DR

This paper introduces a comprehensive calculus for verifying object-oriented programs by combining logic, semantics, alias analysis, and structure specifications, demonstrated through reversing a linked list.

Contribution

It presents a novel calculus integrating multiple components specifically designed for reasoning about object-oriented software properties.

Findings

Successfully proved the linked list reversal algorithm

Demonstrated the calculus's effectiveness in handling object references

Provided a framework for verifying object-oriented program correctness

Abstract

Verifying properties of object-oriented software requires a method for handling references in a simple and intuitive way, closely related to how O-O programmers reason about their programs. The method presented here, a Calculus of Object Programs, combines four components: compositional logic, a framework for describing program semantics and proving program properties; negative variables to address the specifics of O-O programming, in particular qualified calls; the alias calculus, which determines whether reference expressions can ever have the same value; and the calculus of object structures, a specification technique for the structures that arise during the execution of an object-oriented program. The article illustrates the Calculus by proving the standard algorithm for reversing a linked list.