Verifying Object-Oriented Programs That Use Subtypes

Abstract
Object-oriented programming languages like Smalltalk-80 have a generic invocation mechanism that allows code to work on instances of many different types. In this dissertation we show how to write formal specifications of functions that use generic invocation and give a logic for verifying applicative programs that use generic invocation. Our reasoning techniques formalize informal methods based on the use of subtypes. We give a formal definition of subtype relationships among immutable abstract types, including nondeterministic and incompletely specified types. This definition captures the intuition that each instance of a subtype behaves like some instance of that type's supertypes. We show how to write specifications of functions that use generic invocation by allowing instances of subtypes as arguments. We also simplify verification by separately checking that each expression's value is an instance of a subtype of the expression's type. Keywords: Programming languages, Object-oriented, Smalltalk, Specification, Subtype, Type checking, Abstract type, Generic invocation, Message passing, Inclusion polymorphism.

This publication has 0 references indexed in Scilit: