Towards a Calculus of Object Programs
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.
Cite
@article{arxiv.1107.1999,
title = {Towards a Calculus of Object Programs},
author = {Bertrand Meyer},
journal= {arXiv preprint arXiv:1107.1999},
year = {2011}
}