Logo image
Back
Modular Reasoning in an Object-Oriented Refinement Calculus
Book chapter   Peer reviewed

Modular Reasoning in an Object-Oriented Refinement Calculus

Mark Utting and Ken Robinson
Mathematics of Program Construction: 2nd International Conference, Oxford UK, June 29-July 3 1992 Proceedings, pp.344-367
International Conference on the Mathematics of Program Construction, 2nd (Oxford, United Kingdom)
Lecture Notes in Computer Science (LNCS), 669, Springer Berlin Heidelberg
1993
DOI: https://doi.org/10.1007/3-540-56625-2_22
url
https://doi.org/10.1007/3-540-56625-2_22View
Published Version

Abstract

Computation Theory and Mathematics programming techniques algorithm analysis
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.

Details

Metrics

562 Record Views
Logo image