Modular reasoning in an object-oriented refinement calculus

Abstract

Object-oriented languages typically use late binding for procedure calls on objects. This raises a potential problem for programmers who wish to reason about their programs, because the effects of a procedure call cannot always be determined statically. In this paper we develop a simple model of procedure invocation for object-oriented languages based on the refinement calculus [Morgan and Robinson 87] and define the minimum requirements for a system to support modular reasoning. In such systems, reasoning about procedure calls is easier, because the behaviour of a procedure call with arguments of type T can be used as an approximation to its behaviour on more specialised arguments.