A complete algebraic characterization of behavioral subtyping

We present a model-theoretic study of correct behavioral subtyping for firs t-order, deterministic, abstract data types with immutable objects. For suc h types, we give a new algebraic criterion for proving correct behavioral s ubtyping that is both necessary and sufficient. This proof technique handle s incomplete specifications by allowing proofs of correct behavioral subtyp ing to be based on comparison with one of several paradigmatic models. It c ompares a model to a selected paradigm with a generalization of the usual n otion of simulation relations. This generalization is necessary for specifi cations that are not term-generated and that use multiple dispatch. However , we also show that the usual notion of simulation gives a necessary and su fficient proof technique for the special cases of term-generated specificat ions and specifications that only use single dispatch.