Equational Reasoning with Subtypes
				  by
		   Gary T. Leavens and Don Pigozzi

			       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.

Keywords: Behavioral subtyping, equational logic, proof theory.


2001 CR Categories:
D.3.3 [Programming Languages]
 Language Constructs and Features --- Abstract data types,
  classes and objects; 
F.3.1 [Logics and Meanings of Programs]
 Specifying and Verifying and Reasoning about Programs ---
  Logics of programs, specification techniques;
F.3.2 [Logics and Meanings of Programs]
 Semantics of Programming Languages --- algebraic approaches to semantics;
F.3.3 [Logics and Meanings of Programs]
 Studies of Program Constructs --- object-oriented constructs;
F.4.1 [Mathematical Logic and Formal Languages]
 Mathematical Logic --- proof theory, model theory.

Copyright (c) 2002 by Gary T. Leavens and Don Pigozzi.