A Hoare-Calculus for an Object-Oriented Language

Bernhard Reus

(University of Sussex)

A new Hoare-calculus for a simple (Java-like) object-oriented language is presented that includes methods and object creation. In the assertions no explicit representation of state has to be used since the calculus is inspired by America and de Boer's approach without global store and uses the components-as-array-trick to handle aliasing. The calculus can be adapted to OCL (Object Constraint Language which is part of UML). This is joint work with Martin Wirsing
Tuesday 13th February 2001, 14:00
Robert Recorde Room
Department of Computer Science