Verifying Object-Oriented Programs That Use Subtypes
MASSACHUSETTS INST OF TECH CAMBRIDGE LAB FOR COMPUTER SCIENCE
Pagination or Media Count:
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 types 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 expressions value is an instance of a subtype of the expressions type. Keywords Programming languages, Object-oriented, Smalltalk, Specification, Subtype, Type checking, Abstract type, Generic invocation, Message passing, Inclusion polymorphism.
- Computer Programming and Software