archives

A Complete Algebraic Characterization of Behavioral Subtyping


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

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.

Full text available as:Postscript
Adobe PDF

Abstract

A Complete Algebraic Characterization of Behavioral Subtyping
by
Gary T. Leavens and Don Pigozzi
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.
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.

Subjects:All uncategorized technical reports
ID code:00000206
Deposited by:Staff Account on 11 November 1999



Contact site administrator at: ssg@cs.iastate.edu