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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Feb 01, 1989
Accession Number
ADA209118

Entities

People

  • Gary T. Leavens

Organizations

  • Massachusetts Institute of Technology

Tags

Communities of Interest

  • Ground and Sea Platforms

DTIC Thesaurus Topics

  • Classification
  • Computer Programming
  • Computer Science
  • Computers
  • Construction
  • Engineering
  • High Level Languages
  • Information Processing
  • Language
  • Military Research
  • New York
  • Object Oriented Programming
  • Object-Oriented Programming Language
  • Programming Languages
  • Recursive Functions
  • Security
  • Software Development

Fields of Study

  • Computer science
  • Engineering

Readers

  • Computational Linguistics
  • Database Systems and Applications