Subtyping, Modular Specification, and Modular Verification for Applicative Object-Oriented Programs

Date
1994-09-01
Authors
Leavens, Gary
Weihl, William
Journal Title
Journal ISSN
Volume Title
Publisher
Altmetrics
Authors
Research Projects
Organizational Units
Computer Science
Organizational Unit
Journal Issue
Series
Abstract

We present a formal specification language and a formal verification logic for a simple object-oriented programming language. The language is applicative and statically typed, and supports subtyping and message-passing. The verification logic relies on a behavioral notion of subtyping that captures the intuition that a subtype behaves like its supertypes. We give a formal definition for legal subtype relations, based on the specified behavior of objects, and show that this definition is sufficient to ensure the soundness of the verification logic. The verification logic reflects the way programmers reason informally about object-oriented programs, in that it allows them to use static type information, which avoids the need to consider all possible run-time subtypes. We also show that the logic does not require reverification of unchanged code when legal subtypes are added to a program.

Description

© Gary T. Leavens and William E. Weihl, 1992, 1993, 1994. All rights reserved. Much of this report will appear in Acta Informatica, and so the copyright for those portions will be assumed by the Springer-Verlag.

Keywords
verification, specification, supertype abstraction, subtype, message passing, polymorphism, type checking, modularity, soundness, object-oriented, abstract data type
Citation
DOI
Source
Collections