A proof outline logic for object-oriented programming

This paper describes a proof outline logic that covers most typical object-oriented language constructs in the presence of inheritance and subtyping. The logic is based on a weakest precondition calculus for assignments and object allocation which takes field shadowing into account. Dynamically bound method calls are tackled with a variant of Hoare's rule of adaptation that deals with the dynamic allocation of objects in object-oriented programs. The logic is based on an assertion language that is closely tailored to the abstraction level of the programming language.