Behavioral Subtyping, Specification Inheritance, and Modular Reasoning

Date
2006-09-03
Authors
Leavens, Gary
Naumann, David
Journal Title
Journal ISSN
Volume Title
Publisher
Source URI
Altmetrics
Authors
Research Projects
Organizational Units
Computer Science
Organizational Unit
Journal Issue
Series
Abstract

Behavioral subtyping is an established idea that enables modular reasoning about behavioral properties of object-oriented programs. It requires that syntactic subtypes are behavioral refinements. It validates reasoning about a dynamically-dispatched method call, say E.m(), using the specification associated with the static type of the receiver expression E. For languages with references and mutable objects the idea of behavioral subtyping has not been rigorously formalized as such, the standard informal notion has inadequacies, and exact definitions are not obvious. This paper formalizes behavioral subtyping and supertype abstraction for a Java-like sequential language with classes, interfaces, exceptions, mutable heap objects, references, and recursive types. Behavioral subtyping is proved sound and semantically complete for reasoning with supertype abstraction. Specification inheritance, as used in the specification language JML, is formalized and proved to entail behavioral subtyping.

Description
<p>Copyright © 2006 by Gary T. Leavens and David A. Naumann</p>
Keywords
Behavioral subtyping, supertype abstraction, specification inheritance, modularity, specification, verification, state transformer, dynamic dispatch, invariants, Eiffel language, JML language
Citation
Collections