Equational Reasoning with Subtypes







Deposit Papers 


Leavens, Gary T. and Pigozzi, Don (2002) Equational Reasoning with Subtypes. Technical Report TR02-07, Computer Science, Iowa State University.

Full text available as:Adobe PDF


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.
Subjects:Software: SOFTWARE ENGINEERING (K.6.3): Requirements/Specifications (D.3.1)
Software: SOFTWARE ENGINEERING (K.6.3): Software/Program Verification (F.3.1)
Software: PROGRAMMING LANGUAGES: Formal Definitions and Theory (D.2.1, F.3.1-2, F.4.2-3)
Software: PROGRAMMING LANGUAGES: Language Constructs and Features (E.2)
Theory of Computation: COMPUTATION BY ABSTRACT DEVICES: Models of Computation (F.4.1)
ID code:00000283
Deposited by:Gary T. Leavens on 05 August 2002
Alternative Locations:

Contact site administrator at: