Leavens, Gary T. and Pigozzi, Don (1999) A Complete Algebraic Characterization of Behavioral Subtyping. Technical Report TR96-15a, Department of Computer Science, Iowa State University.
A Complete Algebraic Characterization of Behavioral Subtyping
Gary T. Leavens and Don Pigozzi
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
Keywords: behavioral subtype, subtyping, behavior, realization,
observable equivalence, simulation, abstract data type,
single dispatch, multiple dispatch, multimethod.
1994 CR Categories:
D.3.3 [Programming Languages]
Language Constructs --- Abstract data types;
F.3.2 [Logics and Meanings of Programs]
Semantics of Programming Languages --- algebraic approaches to semantics;
F.3.2 [Mathematical Logic and Formal Languages]
Mathematical Logic --- model theory.
1991 Mathematics Subject Classification.
Primary: 68Q65 Secondary: 68N05, 68N15, 68Q60.
Contact site administrator at: firstname.lastname@example.org