2011/07/11 by Bertrand Meyer, Meyer, Bertrand
Computer Science · #Advanced Software Engineering Methodologies #D.2.4 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Programming Languages (cs.PL) #Software Engineering (cs.SE) #Software Engineering Research #cs.LO #cs.PL #cs.SE
paper · pdf · doi:10.48550/arxiv.1107.1999
openalex publication_date 2011/07/11 · arxiv created 2011/07/17 · arxiv updated 2011/07/19 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.