[Prev][Next][Index][Thread]

Stability in OO type system

Date: Mon, 10 Feb 92 15:39:32 EST

Hi. 

I am looking for references to a notion of "stable" class hierarchies
in a sense vaguely sketched below. "Stability" may actually be the
wrong word because of its many different although related
connotations.  This appears to be a list to bring up this question and
perhaps discuss the issue.

We were discussing a "stability" notion for a statically typed paper
OO language that has records, union types and parametrization (and of
course multiple inheritance). I have co-developed and implemented a
dynamically typed language with records and unions earlier [ASDL, IEEE
SW 1/89] in which the "reuse" relation falls into two disjoint parts:
"inherited" (specialized/extended, records) and "adopted"
(generalized/restricted, unions) and which requires the obvious
subtyping and semantic restrictions.  The "reuse" relation thus
extends the usual inheritance relation and defines a direction for
defaults (signatures, specifications, implementations) to "flow" into
classes unless explicitly and consistently overwritten by "own"
definitions. The language then was based on ideas of Cardelli's 84
paper on multiple inheritance etc but we took unions instead of
disjoint unions and made specialization and generalization total
operations on classes etc. The typing issues in the current context
seem clearer than the control of "reuse" in the above sense.  We would
like stability to help here. 

Although we would like our OO language to be imperative, thinking
about the pure sublanguage along order-sorted algebra lines seems most
appropriate, at least to me, for understanding the typing and semantic
issues involved.  In this setting an extension of the OBJ3 approach
with union sorts seems straighforward by means of hierarchical
specifications (for generating the union sorts by, and restricting
their behavior to, enrichments described in a second level only).

Now we would like to call a 
	
	OO program "stable" iff: 

	changes locally consistent/correct imply 
              global consistency/correctness *in-the-large*. 

For a vague but not surprising interpretation of "change", "local"
and "consistency" see below. Moreover we would like to call our (an)

	OO language "stable" iff:

	its stable programs are closed under locally consistent changes.

This perhaps motivates the use of the term. In other words we hope to
obtain sufficient but not too restrictive constraints for stability as
part of formal language semantics.

By "changes" I mean (functorial) program development steps like
renaming, specialization and generalization (adding certain classes in
locally restricted ways), enrichment, restriction, change of
implementations etc. At least in the algebraic-categorical approaches
to OOL semantics these are well-elaborated concepts and I'm sure in
other approaches less known to me, too.

"Consistency" is meant to include well-typing and semantic consistency
(when specs are changed). "Correctness" relates to implementation
correctness (when implementations are changed).  In the order-sorted
algebra setting, most of this would be based on conditional equations
and their satisfaction. Now "local" consistency would mean semantic
constraints for above changes that are expressed only in terms of the
relation of a new or modified class to its direct super- and
subclasses (we want to use name equivalence/conformance rather than
structural equivalence/conformance for our subtyping relation for
now). This notion of locality should not be mistaken to refer only to
the own signature and implementation of a directly related class. We
may have to include indirectly reused behavior but we want
independence of reasoning about the source and distribution of this
behaviour in the class hierarchy.

I would hope that an appropriately introduced notion of stability
would make classes somewhat independent of the global structure
in-the-large, would lead to controlled reuse, and thus would
complement the notion of encapsulation of implementations in-the-small
that the ADT aspect of classes supports.

All of this seems dusty work in order-sorted algebras but
straightforward.
Is it possible that I read about this some time ago?

-- Heinz

Heinz W. Schmidt                            ,--_|\ hws@csis.dit.csiro.au
CSIRO Division of Information Technology & /      \    tel (06) 275-0974
Australian National University, Canberra   \_,--_*/    fax (06) 257-1052
                                                 v