Equational Reasoning with Subtypes

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

Using equational logic as a specification language, we investigate the proof theory of behavioral subtyping for object-oriented abstract data types with immutable objects and deterministic methods that can use multiple dispatch. In particular, we investigate a proof technique for correct behavioral subtyping in which each subtype's specification includes terms that can be used to coerce its objects to objects of each of its supertypes. We show that this technique is sound, using our previous work on the model theory of such abstract data types. We also give an example to show that the technique is not complete, even if the methods do not use multiple dispatch, and even if types specified are term-generated. In preparation for the results on equational subtyping we develop the proof theory of a richer form of equational logic that is suitable for dealing with subtyping and behavioral equivalence. This gives some insight into question of when our proof techniques can be make effectively computable, but in general behavioral consequence is not effectively computable.

Description
Keywords
Behavioral subtyping, equational logic, proof theory
Citation
DOI
Source
Collections