A Hoare-Calculus for an OO-language

Bernhard Reuss

A Hoare-calculus for a simple object-oriented language is presented. In
the assertions no explicit representation of state is necessary since
the calculus is inspired by America and de Boer's  approach without
global store. Special triples for methods are in use to allow for
interface specifications (cf. Poetzsch-Heffter & Mueller). Garbage
collection is not possible yet but hopefully techniques proposed by
Calcagno, Isthiaq and O'Hearn can be used. The approach is extendable to
OCL (Object Constraint Language) and may thus be applied to verify
partial correctness of (simple) Java programs with respect to
OCL-specifications.

This work in progress in collaboration with Martin Wirsing and Rolf
Hennicker, LMU Munich.