Aliasproblematikk innen Hoare-logikk for objektorientert programmering

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