On simulation, subtyping and substitutability in sequential object systems

Abstract

The aim of this article is to clarify the concepts of behavioural subtype and substitutability that are used to establish the safety of dynamic binding and run-time polymorphism in object-oriented programming. A new model of object behaviour is introduced and used to define the states of an object and the notion of object type. A notion of simulation between object behaviours is defined and a subtype relation between object types is derived from it. The syntax and structural operational semantics of an elementary OOPL is given, and the concepts of object and type substitutability are defined. It is shown formally that simulation is equivalent to object substitutability and that subtyping is equivalent to type substitutability.