Towards a Calculus of Object Programs
Bertrand Meyer

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Software Engineering Methodologies · Logic, programming, and type systems · Software Engineering Research
