archives

Behavioral Subtyping in Object-Oriented Languages


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

Dhara, Krishna Kishore (1997) Behavioral Subtyping in Object-Oriented Languages. Technical Report TR97-09, Department of Computer Science, Iowa State University.

Full text available as:Postscript
Adobe PDF

Abstract

Behavioral Subtyping in Object-Oriented Languages
by
Krishna Kishore Dhara
Abstract
Modularity and code reuse are two important features of object-oriented
programming.  Modularity means that adding new components does not
require reverification or respecification of existing components.  A common
form of reuse in object-oriented programs is to add new subtypes to existing
types and to invoke already existing procedures with objects of these new
types. In such cases, behavior of programs  that contain these procedures
also depend on the behavior of the new subtype objects.  Reverifying the
code that uses existing procedures whenever new types are added is not
practical and is not modular.  Thus, a notion of behavioral subtyping
that allows sound modular reasoning is important for object-oriented
programming.
In this dissertation, we study behavioral subtyping for arbitrary abstract
data types in the prescence of mutation and aliasing. We propose
two notions of behavioral subtyping. Strong behavioral subtypes have
objects that act like supertype objects in all cases, whereas as weak
behavioral subtypes have objects that only need to act like supertype
objects when manipulated as supertype objects.  Both these notions allow
sound modular reasoning based on the static types of variables in programs.
Weak behavioral subtyping allows conclusions about programs based on the
effects of individual procedures but restricts certain forms of aliasing.
Strong behavioral subtyping allows all forms of aliasing but permits
conclusions based only on the history constraints of the types.  History
constraints are the reflexive and transitive properties preserved by
objects of a type across different states of a program.  We prove that both
these behavioral subtype notions are sufficient for sound modular reasoning.
Keywords: object-oriented programming, behavioral subtype,
abstract data type, mutation, aliasing, modular verification,
supertype abstraction
1996 CR Categories:
D.1.5 [Programming Techniques]  Object-oriented Programming;
D.3.1 [Programming Languages]   Formal Definitions and Theory --- semantics;
D.3.2 [Programming Languages]
Language Classifications --- object-oriented languages;
D.3.3 [Programming Languages]
Language Constructs --- Abstract data types, modules, packages;
F.3.1 [Logics and Meanings of Programs]
Specifying and Verifying and Reasoning about Programs ---
assertions, logics of programs, pre- and post-conditions,
specification techniques, theory, LSL

Subjects:All uncategorized technical reports
ID code:00000155
Deposited by:Staff Account on 08 May 1997



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