Abstract
Various methods for formal program verification have been around for a
long time. Hoare logic is one such formalism for verification of
imperative programs. When aliasing may occur in the programs, which
is usually the case in object-oriented programs, this logic is no
longer sound.
Some solutions to this problem exist, but there are few that allow
high-level reasoning about object-oriented programs, where method- and
functioncalls are far more important than low-level manipulation of
the objects' components.
In this thesis I first give a few examples of low-level solutions to
the alias-problem in Hoare logic. Based on one of these, I then
introduce a new formalism, designed to be used for high-level reasoning
about object-oriented programs using methods and functions rather than
low-level manipulation of object-components.