Publication Date

11-1999

Technical Report Number

TR96-15a

Subjects

Mathematics of Computing, Software, Computer Systems Organization

Abstract

We present a model-theoretic study of correct behavioral subtyping for first-order, deterministic, abstract data types with immutable objects. For such types, we give a new algebraic criterion for proving correct behavioral subtyping that is both necessary and sufficient. This proof technique handles incomplete specifications by allowing proofs of correct behavioral subtyping to be based on comparison with one of several paradigmatic models. It compares a model to a selected paradigm with a generalization of the usual notion of simulation relations. This generalization is necessary for specifications that are not term-generated and that use multiple dispatch. However, we also show that the usual notion of simulation gives a necessary and sufficient proof technique for the special cases of term-generated specifications and specifications that only use single dispatch.

Comments

Copyright © Gary T. Leavens and Don Pigozzi, 1996.

Share

COinS