Reasoning About Object-Oriented Programs That Use Subtypes

Date
1990-07-01
Authors
Leavens, Gary
Journal Title
Journal ISSN
Volume Title
Publisher
Altmetrics
Authors
Research Projects
Organizational Units
Computer Science
Organizational Unit
Journal Issue
Series
Abstract

Programmers informally reason about object-oriented programs by using subtype relationships to classify the behavior of objects of different types and by letting supertypes stand for all their subtypes. We describe formal specification and verification techniques for such programs that mimic these informal ideas. Our techniques are modular and extend standard techniques for reasoning about programs that use abstract data types. Semantic restrictions on subtype relationships guarantee the soundness of these techniques.

Description
Keywords
verification, specification, subtype, message passing, polymorphism, type checking, modularity
Citation
DOI
Source
Collections