topical media & game development
object-oriented programming
Abstract data types
The history of programming languages may be characterized
as the genesis of increasingly powerful abstractions
to aid the development of reliable programs.
Abstract data types
8
- abstraction and types
- algebraic specification
- modules versus classes
- types as constraints
Additional keywords and phrases:
control abstractions, data abstractions,
compiler support,
description systems,
behavioral specification,
implementation specification
slide: Abstract data types
In this chapter we will look at the notion of
abstract data types, which may be regarded as
an essential constituent of object-oriented modeling.
In particular, we will study the notion of data abstraction
from a foundational perspective, that is based on
a mathematical description of types.
We start this chapter by discussing the notion of
types as constraints.
Then, we look at the (first order) algebraic specification of
abstract data types, and
we explore the trade-offs between the traditional
implementation of abstract data types by employing modules
and the object-oriented approach employing classes.
We conclude this chapter by exploring the
distinction between classes and types,
as a preparation for the treatment of
(higher order) polymorphic type theories for object
types and inheritance in the next chapter.
object-oriented programming
Abstraction and types
subsections:
The concern for abstraction may be regarded as the driving
force behind the development of programming languages
(of which there are astoundingly many).
In the following we will discuss the role
of abstraction in programming,
and especially the importance of types.
We then briefly look at what mathematical means
we have available to describe types from a foundational
perspective and what we may (and may not) expect
from types in object-oriented programming.
Abstraction in programming languages
In [Shaw84], an overview is given of how increasingly powerful
abstraction mechanisms have shaped the programming
languages we use today.
See slide [8-abstraction].
Abstraction -- programming methodology
- control abstractions -- structured programming
- data abstraction -- information hiding
The kind of abstraction provided by ADTs can be supported
by any language with a procedure call mechanism
(given that appropriate protocols are developed
and observed by the programmer). [DT88]
slide: Abstraction and programming languages
Roughly, we may distinguish between two categories
of abstractions: abstractions that aid in specifying
control (including subroutines, procedures,
if-then-else constructs, while-constructs,
in short the constructs promoted by the school of
structured programming in their battle against
the goto);
and abstractions that allow us to hide
the actual representation of the data employed
in a program (introduced to support the information hiding
approach, originally advocated in [Parnas72a]).
Although there is clearly a pragmatic interest
involved in developing and employing such abstractions,
the concern with abstraction (and consequently types)
is ultimately motivated by a concern with
programming methodology and, as observed in [DT88],
the need for reliable and maintainable software.
However, the introduction of language features
is also often motivated by programmers' desires
for ease of coding and naturalness of expression.
In the same vein, although types were originally considered
as a convenient means to assist the compiler in producing
efficient code, types have rapidly been recognized
as a way in which to capture the meaning of a program in an
implementation independent way.
In particular, the notion of abstract data types
(which has, so to speak, grown out of data abstraction)
has become a powerful device (and guideline)
to structure large software systems.
In practice, as the quotation from [DT88]
in slide [8-abstraction] indicates,
we may employ the tools developed for structured programming
to realize abstract data types in a program,
but with the obvious disadvantage that we must rely on
conventions with regard to the reliability of these
realizations.
Support for abstract data types (support in the sense
as discussed in section [paradigms]) is offered (to some extent)
by languages such as Modula-2 and Ada by means of a syntactic
module or package construct,
and (to a larger extent) by object-oriented languages
in the form of object classes.
However, both realizations are of a rather ad hoc
and pragmatic nature,
relying in the latter case on the metaphor of encapsulation
and message passing.
The challenge to computer science in this area is
to develop a notion of types capturing the power
of abstract data types in a form that is adequate
both from a pragmatic point of view (in the sense
of allowing efficient language support) and from
a theoretical perspective (laying the foundation
for a truly declarative object-oriented approach
to programming).
A foundational perspective -- types as constraints
Object-oriented programming may be regarded as
a declarative method of programming,
in the sense that it provides a computation model
(expressed by the metaphor of encapsulation and message
passing) that is independent of a particular implementation model.
In particular, the inheritance subtype relation may
be regarded as a pure description of the relations
between the entities represented by the classes.
Moreover, an object-oriented approach favors the
development of an object model that bears close resemblance
to the entities and their relations living in the
application domain.
However, the object-oriented
programming model is rarely introduced with the
mathematical precision characteristic of descriptions
of the other declarative styles,
for example
the functional and logic programming model.
Criticizing, [DT88] remark that {\em OOP is generally
expressed in philosophical terms, resulting
in a proliferation of opinions concerning what
OOP really is}.
From a type-theoretical perspective, our interest
is to identify abstract data types as elements
of some semantic (read mathematical) domain
and to characterize their properties in an unambiguous
fashion.
See slide [8-mathematical].
Abstract data types -- foundational perspective
- unambiguous values in some semantic domain
Mathematical models -- types as constraints
- algebra -- set oriented
- second order lambda calculus -- polymorphic types
- constructive mathematics -- formulas as types
slide: Mathematical models for types
There seems to be almost
no limit to the variety and sophistication of the
mathematical models proposed to characterize abstract
data types and inheritance.
We may make a distinction
between first order approaches
(based on ordinary set theory) and higher
order approaches (involving typed lambda calculus
and constructive logic).
The algebraic approach is a quite well-established
method for the formal specification of abstract data types.
A type (or sort) in an algebra corresponds to a set
of elements upon which the operations of the
algebra are defined.
In the next section, we will look at how equations
may be used to characterize the behavioral aspects of
an abstract data type modeled by an algebra.
Second order lambda calculus has been used to
model information hiding and the polymorphism supported
by inheritance and templates.
In the next chapter we will study this approach in more
detail.
In both approaches, the meaning of a type is
(ultimately) a set of elements satisfying certain restrictions.
However, in a more abstract fashion, we may
regard a type as specifying a constraint.
The better we specify the constraint, the more tightly
the corresponding set of elements will be defined
(and hence the smaller the set).
A natural consequence of the idea of types as constraints
is to characterize types by means of logical formulas.
This is the approach taken by type theories based
on constructive logic, in which the notion
of formulas as types plays an important role.
Although we will not study type theories
based on constructive logic explicitly, our
point of view is essentially to regard
types as constraints, ranging from purely
syntactical constraints (as expressed in a signature)
to semantic constraints (as may be expressed in contracts).
From the perspective of types as constraints,
a typing system may
contribute to a language framework guiding
a system designer's conceptualization and supporting
the verification (based on the formal properties
of the types employed) of the consistency of the descriptive information
provided by the program.
Such an approach is to be preferred (both from
a pragmatic and theoretical point of view)
to an ad hoc approach employing special annotations and
support mechanisms, since these may become quite
complicated and easily lead to unexpected
interactions.
Formal models
There is a wide variety of formal models available
in the literature.
These include algebraic models (to characterize the meaning
of abstract data types), models based on
the lambda-calculus and its extensions (which are primarily
used for a type theoretical analysis of object-oriented
language constructs),
algebraic process calculi (which may be used to characterize the
behavior of concurrent objects),
operational and denotational semantic models
(to capture structural and behavioral properties of programs),
and various specification languages based on
first or higher-order logics
(which may be used to specify the desired behavior
of collections of objects).
We will limit ourselves to studying
algebraic models capturing the properties of abstract data
types and objects (section [algebra]),
type calculi based on typed extensions of the lambda calculus
capturing the various flavors of polymorphism and subtyping
(sections [flavors]--[self-reference]), and
an operational semantic model characterizing the behavior
of objects sending messages (section [behavior]).
Both the algebraic and type theoretical models
are primarily intended to clarify the means we have
to express the desired behavior of objects
and the restrictions that must be adhered to
when defining objects and their relations.
The operational characterization of object behavior,
on the other hand, is intended to give a more
precise characterization of the notion of state
and state changes underlying the verification
of object behavior by means of assertion logics.
Despite the numerous models introduced there are
still numerous approaches not covered here.
One approach worth mentioning is the work based
on the pi-calculus.
The pi-calculus is an extension of algebraic
process calculi that allow for communication via
named channels.
Moreover, the pi-calculus allows for a notion
of migration and the creation and renaming
of channels.
A semantics of object-based languages based
on the pi-calculus is given in
[Walker90].
However, this semantics does not cover
inheritance or subtyping.
A higher-order object-oriented programming
language based on the pi-calculus is
presented in [PRT93].
Another approach of interest, also based on process calculi,
is the object calculus (OC) described in [Nier93].
OC allows for modeling the operational
semantics of concurrent objects.
It merges the notions of agents, as used in process calculi,
with the notion of functions, as present in the lambda calculus.
For alternative models the reader may look
in the {\tt comp.theory} newsgroup to which information
concerning formal calculi for OOP is posted
by Tom Mens of the Free University, Brussels.
Objectives of typed OOP
Before losing ourselves in the details
of mathematical models of types, we must reflect
on what we may expect from a type system
and what not (at least not currently).
From a theoretical perspective our ideal is,
in the words of [DT88], to arrive at a simple type theory
that provides a consistent and flexible framework
for system descriptions
(in order to provide the programmer with sufficient descriptive
power and to aid the construction of useful and
understandable software, while allowing the efficient utilization
of the underlying hardware).
Objectives of typed OOP -- system description
- packaging in a coherent manner
- flexible style of associating operations with objects
- inheritance of description components -- reuse, understanding
- separation of specification and implementation
- explicit typing to guide binding decisions
slide: Object orientation and types
The question now is, what support does a typing
system provide in this respect.
In slide [8-objectives], a list is given of aspects in which a typing system
may be of help.
One important benefit of regarding ADTs as
real types is that realizations of ADTs
become so-called first class citizens,
which means that they may be treated as any other
value in the language, for instance being passed
as a parameter.
In contrast, syntactic solutions (such as the module
of Modula-2 and the package of Ada) do not allow this.
Pragmatically, the objective of a type system is (and has been)
the prevention of errors.
However, if the type system lacks expressivity,
adequate control for errors may result in becoming
over-restrictive.
In general, the more expressive the type system
the better the support that the compiler may offer.
In this respect, associating constructors with types
may help in relieving
the programmer from dealing with simple but necessary
tasks such as the initialization of complex structures.
Objects, in contrast to modules or packages, allow
for the automatic (compiler supported) initializations
of instances of (abstract) data types,
providing the programmer with relief from an error-prone
routine.
Another area in which a
type system may make the life of a programmer easier
concerns the association of operations with objects.
A polymorphic type system is needed to
understand
the automatic dispatching for virtual
functions and the opportunity of overloading functions,
which
are useful mechanisms to control the complexity
of a program, provided they are well understood.
Reuse and understanding are promoted by allowing
inheritance and refinement of description components.
(As remarked earlier, inheritance and refinement may be regarded as the
essential contribution of object-oriented programming
to the practice of software development.)
It goes without saying that
such reuse needs a firm
semantical basis in order to achieve the goal
of reliable and maintainable software.
Another important issue for which a powerful
type system can provide support is the separation
of specification and implementation.
Naturally, we expect our type system to support
type-safe separate compilation.
But in addition, we may think of allowing
multiple implementations of a single (abstract type)
specification.
Explicit typing may then be of help in choosing
the right binding when the program is actually executed.
For instance in a parallel environment,
behavior may be realized in a number of ways
that differ in the degree to which they affect locality
of access and how they affect, for example, load balancing.
With an eye to the future, these are problems
that may be solved with a good type system
(and accompanying compiler).
One of the desiderata for a type system
for OOP, laid down in [DT88],
is the separation of a behavioral hierarchy
(specifying the behavior of a type in an abstract sense)
and an implementation hierarchy (specifying the
actual realization of that behavior).
Separation is needed
to accommodate the need for multiple realizations
and
to resolve the tension between subtyping
and inheritance (a tension we have already noted
in sections [theme]
and [contracts]).
Remark
In these chapters we cannot hope to do more than
get acquainted with the
material needed
to understand the problems involved in developing
a type system for object-oriented programming.
For an alternative approach, see [Palsberg94].
object-oriented programming
Algebraic specification
subsections:
Algebraic specification techniques have
been developed as a means to specify the design
of complex software systems in a formal way.
The algebraic approach has been motivated by
the notion of information hiding
put forward in [Parnas72a] and the ideas
concerning abstraction expressed in [Ho72].
Historically, the ADJ-group (see Goguen et al., 1978) provided
a significant impetus to the algebraic approach
by showing that abstract data types may be interpreted
as (many sorted) algebras.
(In the context of algebraic specifications the
notion of sorts has the same meaning as types.
We will, however, generally speak of types.)
As an example of an algebraic specification,
look at the module defining the data type Bool,
as given in slide [8-Bool].
Algebraic specification -- ADT
Bool
adt bool is
functions
true : bool
false : bool
and, or : bool * bool -> bool
not : bool -> bool
axioms
[B1] and(true,x) = x
[B2] and(false,x) = false
[B3] not(true) = false
[B4] not(false) = true
[B5] or(x,y) = not(and(not(x),not(y)))
end
slide: The ADT Bool
In this specification two constants are introduced
(the zero-ary functions
true and false), three functions (respectively
and, or and not).
The or function is defined by employing not
and and, according to a well-known logical law.
These functions may all be considered to be (strictly)
related to the type bool.
Equations are used to specify the desired characteristics
of elements of type bool.
Obviously, this specification may mathematically be interpreted
as (simply) a boolean algebra.
Mathematical models
The mathematical framework of algebras allows for
a direct characterization of the behavioral
aspects of abstract data types by means of equations,
provided the specification is consistent.
Operationally, this allows for the execution
of such specifications by means of term rewriting,
provided that some (technical) constraints are met.
The model-theoretic semantics of algebraic
specifications centers around the notion
of initial algebras, which gives
us the preferred model of a specification.
To characterize the behavior of objects
(that may modify their state) in an algebraic way,
we need to extend the basic framework of initial
algebra models either by allowing
so-called multiple world semantics or by
making a distinction between hidden and observable
sorts (resulting in the notion of
an object as an abstract machine).
As a remark, in our treatment we obviously cannot
avoid the use of some logico-mathematical formalism.
If needed, the concepts introduced will be explained
on the fly.
Where this does not suffice, the interested reader
is referred to any standard textbook on mathematical
logic for further details.
Signatures -- generators and observers
Abstract data types may be considered as modules
specifying the values and functions belonging
to the type.
In [Dahl92], a type T is characterized as a tuple specifying
the set of elements constituting the type T
and the collection of functions related
to the type T.
Since constants may be regarded as zero-ary functions
(having no arguments), we will speak of a signature
$%S$ or $%S_T$ defining a particular type T.
Also, in accord with common parlance, we will speak
of the sorts $s \e %S$, which are the sorts (or types)
occurring in the declaration of the functions in $%S$.
See slide [8-signature].
Signature -- names and profiles
$%S$
- $ f : s_1 \* ... \* s_n -> s $
Functions -- for $T$
- constants -- $c : -> T$
- producers -- $g : s_1 \* ... \* s_n -> T$
- observers -- $f : T -> s_i$
Type -- generators
- $ %S_T = P_T \cup O_T$, $C_T \subset P_T$, $P_T \cap O_T = \emptyset$
slide: Algebraic specification
A signature specifies the names and (function) profiles
of the constants and functions of a data type.
In general, the profile of a function is specified as
- $ f : s_1 \* ... \* s_n -> s $
where $ s_i (i=1..n) $ are the sorts defining
the domain (that is the types of the arguments)
of the function f, and s is the sort defining the codomain
(or result type) of f.
In the case $ n=0 $ the function f may be regarded as
a constant. More generally, when $ s_1,...,s_n $ are all
unrelated to the type T being defined, we may regard
f as a relative constant.
Relative constants are values that are assumed to
be defined in the context
where the specification is being employed.
The functions related to a data type T may be discriminated
according to their role in defining T.
We distinguish between producers $ g \e P_T $,
that have the type T under definition as their result
type, and observers $f \e O_T$, that have T
as their argument type and deliver a result of
a type different from T.
In other words, producer functions define how
elements of T may be constructed.
(In the literature one often speaks of constructors,
but we avoid this term because it already has a
precisely defined meaning in the object-oriented
programming language C++.)
In contrast, observer functions do not produce
values of T, but give instead information
on some particular aspect of T.
The signature $ %S_T $ of a type T is uniquely defined
by the union of producer functions $ P_T $ and
observer functions $ O_T $.
Constants of type T are regarded as a subset of
the producer functions $P_T$ defining T.
Further, we require that the collection of producers is
disjoint from the collection of observers for T,
that is $P_T \cap O_T = \emptyset$.
Generators
The producer functions actually defining the
values of a data type T are called the
generator basis of T, or generators of T.
The generators of T may be used to enumerate the
elements of T, resulting in the collection of T values
that is called the generator universe in [Dahl92].
See slide [8-basis].
Generators -- values of $T$
T
- generator basis -- $G_T = { g \e P_T }$
- generator universe -- $GU_T = { v_1, v_2, ... }$
Examples
- $G_{Bool} = { t, f }$, $GU_{Bool} = { t, f }$
- $G_{Nat} = { 0, S }$, $GU_{Nat} = { 0, S 0, SS 0, ... }$
- $G_{Set_{A} } = { \emptyset, add }$, $GU_{Set_{A} = { \emptyset, add(\emptyset,a), ... }$
slide: Generators -- basis and universe
The generator universe of a type T consists of the
closed (that is variable-free) terms that may be constructed
using either constants or producer functions of T.
As an example, consider the data type Bool with
generators t and f.
Obviously, the value domain of Bool, the
generator universe $GU_{Bool}$ consists only of the values
t and f.
As another example, consider the data type Nat
(representing the natural numbers) with generator basis
$G_{Nat} = { 0, S }$, consisting of the constant 0
and the successor function $S : Nat -> Nat$
(that delivers the successor of its argument).
The terms that may be constructed by $G_{Nat}$ is the
set $GU_{Nat} = { 0, S 0, SS 0, ... }$,
which uniquely corresponds to the natural numbers
${ 0, 1, 2, ... }$.
(More precisely,
the natural numbers are isomorphic with $GU_{Nat}$.)
In contrast, given a type A
with element a, b, ..., the generators of $Set_{A}$ result in
a universe that contains terms such as
$add(\emptyset,a)$ and $add(add(\emptyset,a),a)$
which we would like
to identify, based on our conception of a set
as containing only one exemplar of a particular value.
To effect this we need additional equations imposing
constraints expressing what we consider as the
desired shape (or normal form) of the values
contained in the universe of T.
However, before we look at how to extend a signature
$%S$ defining T with equations defining the
(behavioral) properties of T we will look
at another example illustrating how the choice
of a generator basis may affect the structure
of the value domain of a data type.
In the example presented in slide [8-Seq],
the profiles are given of the functions
that may occur in the signature specifying sequences.
(The notation _ is used to indicate parameter positions.)
Sequences
- $ %e : seq T$
empty
- $ _ |> _ : seq T \* T -> seq T$
right append
- $ _ <| _ : T \* seq T -> seq T$
left append
- $ _ \. _ : seq T \* seq T -> seq T$
concatenation
- $<< _ >> : T -> seq T$
lifting
- $<< _,...,_ >> : T^{n} -> seq T$
multiple arguments
Generator basis -- preferably one-to-one
- $G_{seq T } = { %e, |> }$, $GU_{seq T } = { %e, %e |> a, %e |> b, ..., %e |> a |> b, ... }$
- $G'_{seq T } = { %e, <| }$, $GU'_{seq T } = { %e, a <| %e , b <| %e, ..., b <| a <| %e, ... }$
- $G''_{seq T } = { %e, \. , << _ >> }$, $GU''_{seq T } = { %e, <>, <>, ,..., %e \. %e, ..., %e \. <> , ... }$
Infinite generator basis
- $G'''_{seq T } = { %e, << _ >>, << _ , _ >>, ... }$, $GU'''_{seq T } = { %e, <>, <>, ,..., <> , ... }$
slide: The ADT Seq
Dependent on which producer functions are selected to
generate the universe of T, the correspondence
between the generated universe and the intended domain
is either one-to-one
(as for G and $G'$) or many-to-one
(as for $G''$).
Since we require our specification to be first-order
and finite, infinite generator bases (such as $G'''$)
must be disallowed, even if they result
in a one-to-one correspondence.
See [Dahl92] for further details.
Equations -- specifying constraints
The specification of the signature of a type
(which lists the syntactic constraints
to which a specification must comply)
is in general not sufficient to characterize
the properties of the values of the type.
In addition, we need to impose semantic constraints
(in the form of equations) to define the meaning
of the observer functions and (very importantly)
to identify the elements of the type domain
that are considered equivalent (based on
the intuitions one has of that particular type).
The equivalence relation -- congruence
- $x = x$ \zline{reflexivity}
- $x = y => y = x$ \zline{symmetry}
- $x = y /\ y = z => x = z$ \zline{transitivity}
- $x = y => f(...,x,...) = f(...,y,...)$
Equivalence classes -- representatives
- abstract elements -- $GU_T /= $
slide: Equivalence
Mathematically, the equality predicate may
be characterized by the properties listed above,
including reflexivity (stating that an element
is equal to itself), symmetry (stating that
the orientation of the formula is not important)
and transitivity (stating that if one element
is equal to another and that element is equal to
yet another, then the first element is also equal to
the latter).
In addition, we have the property that, given
that two elements are equal, the results
of the function applied to them (separately) are
also equal.
(Technically, the latter property makes a congruence
of the equality relation, lifting
equality between elements to the function level.)
See slide [8-equivalence].
Given a suitable set of equations, in addition to
a signature,
we may identify the elements that can be proved
identical by applying the equality relation.
In other words, given an equational theory
(of which the properties stated above must be a part),
we can divide the generator universe of a type T
into one or more subsets,
each consisting of elements that are equal
according to our theory.
The subsets of $GU/=$, that is GU
factored with respect to equivalence,
may be regarded as the abstract elements constituting the type
T,
and from each subset we may choose a concrete
element acting as a representative for the subset
which is the equivalence class of the element.
Operationally, equations may be regarded as
rewrite rules (oriented from left to right),
that allow us to transform a term in which
a term $t_1$ occurs as a subterm into a term
in which $t_1$ is replaced by $t_2$ if $t_1 = t_2$.
For this procedure to be terminating,
some technical restrictions must be met,
amounting (intuitively) to the requirement that the right-hand side
must in some sense be simpler than the left-hand side.
Also, when defining an observer function, we must specify for
each possible generator case an appropriate rewriting rule.
That is, each observer must be able to give
a result for each generator.
The example of the natural numbers, given below, will make
this clear.
Identifying spurious elements by rewriting a term into
a canonical form is somewhat more complex,
as we will see for the example of sets.
Equational theories
To illustrate the notions introduced above,
we will look at specifications of some familiar
types, namely the natural numbers and sets.
In slide [8-Nat], an algebraic specification is given of the natural
numbers (as first axiomatized by Peano).
Natural numbers
Nat
functions
0 : Nat
S : Nat -> Nat
mul : Nat * Nat -> Nat
plus : Nat * Nat -> Nat
axioms
[1] plus(x,0) = x
[2] plus(x,Sy) = S(plus(x,y))
[3] mul(x,0) = 0
[4] mul(x,Sy) = plus(mul(x,y),x)
end
slide: The ADT Nat
In addition to the constant 0 and successor function
S we also introduce a function mul for
multiplication and a function plus for addition.
(The notation Sy stands for application by
juxtaposition; its meaning is simply $S(y)$.)
The reader who does not immediately accept
the specification in slide [8-Nat] as an adequate
axiomatization of the natural numbers must
try to unravel the computation depicted in slide [8-symbolic].
mul(plus(S 0,S 0),S 0) -[2]->
mul(S(plus(S 0,0)), S 0) -[1]->
mul(SS 0,S 0) -[4]->
plus(mul(SS0,0),SS0) -[3]->
plus(0,SS0) -[2*]-> SS0
slide: Symbolic evaluation
Admittedly, not an easy way to compute with
natural numbers, but fortunately term rewriting
may, to a large extent, be automated (and actual calculations
may be mimicked by semantics preserving primitives).
Using the equational theory expressing the properties
of natural numbers, we may eliminate
the occurrences of the functions mul and plus
to arrive (through symbolic evaluation) at something
of the form $S^n 0$ (where n corresponds
to the magnitude of the natural number denoted by the term).
The opportunity of symbolic evaluation by term
rewriting is exactly what has made the algebraic
approach so popular for the specification of software,
since it allows (under some restrictions)
for executable specifications.
Since they do not reappear in what may be considered
the normal forms of terms denoting the naturals
(that are obtained by applying the evaluations induced by the
equality theory),
the functions plus and mul may be regarded as secondary
producers.
They are not part of the generator basis of the type Nat.
Since we may consider mul and plus as secondary
producers at best, we can easily see that when we define
mul and plus for the case 0 and Sx
for arbitrary x, that we have covered all possible (generator) cases.
Technically, this allows us to prove properties of these
functions by using structural induction on the possible generator cases.
The proof obligation (in the case of the naturals) then is to
prove that the property holds for the function applied
to 0 and assuming that the property
holds for applying the function to x, it also
holds for Sx.
As our next example, consider the algebraic
specification of the type $Set_{A}$ in slide [8-Set].
Sets
Set
- $G_{Set_{A} = { \emptyset, add }$
- $GU_{Set_{A} }$ $ = $ ${ 0, add(0,a), ..., add(add(0,a),a), ... }$
Axioms
[S1] $add(add(s,x),y) = add(add(s,y),x)$ commutativity
[S2] $add(add(s,x),x) = add(s,x)$ idempotence
slide: The ADT Set
In the case of sets we have the problem that
we do not start with a one-to-one generator base
as we had with the natural numbers.
Instead, we have a many-to-one generator base,
so we need equality axioms to eliminate spurious
elements from the (generator) universe of sets.
Equivalence classes
$ GU_{ Set _{A} }/= $
- ${ \emptyset }$
- ${ add(0,a), add(add(0,a),a), ... }$
- $...$
- ${ add(add(0,a),b), add(add(0,b),a), ... }$
slide: Equivalence classes for Set
The equivalence classes of $GU_{Set _{A} }/=$
(which is $GU_{Set _{A} }$ factored by the equivalence
relation), each have multiple elements (except
the class representing the empty set).
To select an appropriate representative
from each of these classes (representing the abstract
elements of the type $Set_{A}$) we need
an ordering on terms, so that we can take the smaller
term as its canonical representation.
See slide [8-set-equi].
Initial algebra semantics
In the previous section we have given a rather operational
characterization of the equivalence relation induced by
the equational theory and the process of term rewriting
that enables us to purge the generator universe of a type,
by eliminating redundant elements.
However, what we actually strive for is a mathematical
model that captures the meaning of an algebraic
specification.
Such a model is provided (or rather a class of such models)
by the mathematical structures known as
(not surprisingly) algebras.
A single sorted algebra $|A$ is a structure $ (A,%S) $
where A is a set of values, and $%S$ specifies the signature
of the functions operating on A.
A multi-sorted algebra is a structure $ |A = ( { A_s }_{s \e S }, %S)$
where S is a set of sort names and $A_s$ the set of values belonging
to the sort s.
The set S may be ordered (in which case the ordering
indicates the subtyping relationships between the sorts).
We call the (multi-sorted) structure $|A$ a $\%S$-algebra.
Mathematical model -- algebra
- $%S$-algebra -- $ |A = ( { A_s }_{s \e S }, %S )$
- interpretation -- $ eval : T_{%S} -> |A $
- adequacy -- $ |A |= t_1 = t_2 <=> E |- t_1 = t_2 $
slide: Interpretations and models
Having a notion of algebras, we need to have a way in which
to relate an algebraic specification to
such a structure.
To this end we define an interpretation $eval : T_{%S} -> |A$
which maps closed terms formed by following the rules
given in the specification to elements of the structure $|A$.
We may extend the interpretation eval to include
variables as well (which we write
as $ eval : T_{%S}(X) -> |A$), but then we also need to assume
that an assignment $%h : X -> T_{%S}(X)$ is given,
such that when applying $%h$ to a term t the result
is free of variables, otherwise no interpretation in $|A$ exists.
See slide [8-algebra].
Interpretations
As an example, consider the interpretations
of the specification of Bool and
the specification of Nat, given in slide [8-B-N].
Booleans
- $ |B = ( { tt, ff }, { \neg, / \/ } )$
- $ eval_{|B} : T_{Bool} -> |B = { or |-> \/, and |-> / not |-> \neg }$
Natural numbers
- $ |N = ( \nat , { ++ , + , \star } ) $
- $ eval_{|N} : T_{Nat} -> |N = { S |-> ++ , mul |-> \star, plus |-> + }$
slide: Interpretations of Bool and Nat
The structure $|B$ given above is simply a boolean algebra, with
the operators $\neg$, $ /\ $ and $ \/ $.
The functions not, and and or naturally map to their semantic counterparts.
In addition, we assume that the constants true and false map
to the elements tt and ff.
As another example, look at the structure $|N$ and the
interpretation $eval_{|N}$, which maps
the functions S, mul and plus specified
in Nat in a natural way.
However, since we have also given equations for Nat
(specifying how to eliminate the functions mul and plus)
we must take precautions such that the requirement
$ |N |= eval_{|N}(t_1) =_{|N} eval_{|N}(t_2) <=> E_{Nat} |- t_1 = t_2 $
is satisfied if the structure $ |N $ is to count as an adequate
model of Nat.
The requirement above states
that whenever equality holds for two interpreted
terms (in $ |N $) then these terms must also be provably equal
(by using the equations given in the specification of Nat),
and vice versa.
As we will see illustrated later, many models may exist
for a single specification, all satisfying the requirement
of adequacy.
The question is, do we have a means to select one of these
models as (in a certain sense) the best model.
The answer is yes.
These are the models called initial models.
Initial models
A model (in a mathematical sense) represents the meaning
of a specification in a precise way.
A model may be regarded as stating a commitment with
respect to the interpretation of the specification.
An initial model is intuitively the least committing
model, least committing in the sense
that it imposes only identifications made necessary by
the equational theory of a specification.
Technically, an initial model is a model from which
every other model can be derived by an algebraic mapping
which is a homomorphism.
Initial algebra
- $%S E$-algebra -- $|M = ( T_{%S}/=, %S/=)$
Properties
- no junk -- $ \A a : T_{%S}/= \E t \dot eval_{|M}(t) = a $
- no confusion -- $ |M |= t_1 = t_2 <=> E |- t_1 = t_2 $
slide: Initial models
The starting point for the construction of an initial model
for a given specification with signature $%S$ is to
construct a term algebra $T_{%S}$ with
the terms that may be generated from the signature $%S$
as elements.
The next step is then to factor the universe of generated
terms into equivalence classes, such that
two terms belong to the same class if they can be proven equivalent
with respect to the equational theory of the specification.
We will denote the representative of the equivalence class to
which a term t belongs by $[t]$.
Hence $t_1 = t_2$ (in the model) iff $[t_1] = [t_2]$.
So assume that we have constructed a structure
$ |M = (T_{%S}/=, %S ) $ then; finally, we must define an interpretation,
say $eval_{|M} : T_{%S} -> |M$, that assigns closed
terms to appropriate terms in the term model
(namely the representatives of the equivalence class of that term).
Hence, the interpretation of a function f in the structure $|M$
is such that
$f_{|M}([t_1],...,[t_n]) = [ f(t_1,...,t_n) ] $
where $f_{|M}$ is the interpretation of f in $|M$.
In other words, the result of applying f to terms $t_1,...,t_n$
belongs to the same equivalence class as the result
of applying $f_{|M}$ to the representatives of the
equivalence classes of $t1,...,t_n$.
See slide [8-initial].
An initial algebra model has two important properties,
known respectively as the no junk and no confusion
properties.
The no junk property states that for each element of the
model there is some term for which the interpretation in $|M$
is equal to that element.
(For the $T_{%S}/=$ model this is simply a representative of
the equivalence class corresponding with the element.)
The no confusion property states that if equality of two
terms can be proven in the equational theory of the specification,
then the equality also holds (semantically) in the model,
and vice versa.
The no confusion property means, in other words, that
sufficiently many identifications are made
(namely those that may be proven to hold),
but no more than that (that is, no other than those
for which a proof exists).
The latter property is why we may speak of an initial model
as the least committing model; it simply gives
no more meaning than is strictly needed.
The initial model constructed from the term algebra
of a signature $%S$ is intuitively a very natural model
since it corresponds directly with (a subset of) the
generator universe of $%S$.
Given such a model, other models may be derived from it
simply by specifying an appropriate interpretation.
For example, when we construct a model for the natural
numbers (as specified by Nat) consisting of the
generator universe ${ 0, S 0, SS 0, ... }$
and the operators ${ ++, +, \star }$
(which are defined as $S^n ++ = S^{n+1}$,
${ S^n } \ast { S^m } = S^{ {n \ast m} }$
and $S^n + S^m = S^{n + m}$)
we may simply derive from this model
the structure $ ({ 0,1,2,... }, { ++, +, \star }) $
for which the operations have their standard arithmetical
meaning.
Actually, this structure is also an initial model for
Nat, since we may also make the inverse transformation.
More generally, when defining an initial model only
the structural aspects
(characterizing the behavior of the operators) are
important, not the actual contents.
Technically, this means that initial models
are defined up to isomorphism, that is a mapping to
equivalent models with perhaps different contents
but an identical structure.
Not in all cases is a structure derived from an initial model itself
also an initial model, as shown in the example below.
Example
Consider the specification of Bool as given before.
For this specification we have given the structure
$ |B $ and the interpretation $ eval_{|B} $ which defines
an initial model for Bool. (Check this!)
Structure -- $ |B = ( {{ tt, ff }}, {{ \neg, /\, \/ }} )$
$|B$
- $ eval_{|B} : T_{%S_{Bool} -> |B = { or |-> \/, not |-> \neg }$
- $ eval_{|B} : T_{%S_{Nat} -> |B = { S |-> \neg, mul |-> / plus |-> xor }$
slide: Structure and interpretation
We may, however, also use the structure $|B$ to
define an interpretation of Nat.
See slide [8-structure].
The interpretation $eval_{|B} : T_{Nat} -> |B$ is such
that
$eval_{|B}(0) = ff$,
$eval_{|B}(Sx) = \neg eval_{|B}(x)$,
$eval_{|B}(mul(x,y)) $ $ = eval_{|B}(x) $\hspace{0.2cm} $ /\ $ \hspace{0.2cm} $ eval_{|B}(y)$\hspace{0.3cm} and
$eval_{|B}(plus(x,y)) = xor(eval_{|B}(x),eval_{|B}(y))$,
where $xor(p,q) = (p \/ q) /\ (\neg ( p /\ q ))$.
The reader may wish to ponder on what this interpretation
effects.
The answer is that it interprets Nat as
specifying the naturals modulo 2, which discriminates
only between odd and even numbers.
Clearly, this interpretation defines not an initial model,
since it identifies all odd numbers with ff and all even numbers with tt.
Even if we replace ff by 0 and tt by 1, this is not what we
generally would like to commit ourselves to when we speak
about the natural numbers,
simply because it assigns too much meaning.
Objects as algebras
The types for which we have thus far seen algebraic specifications
(including Bool, Seq, Set and Nat)
are all types of a mathematical kind,
which (by virtue of being mathematical) define
operations without side-effects.
Dynamic state changes, that is side-effects,
are often mentioned as determining the characteristics
of objects in general.
In the following we will explore how we may deal with
assigning meaning to dynamic state changes in an algebraic framework.
Let us look first at the abstract data type stack.
The type stack may be considered as one of the `real life'
types in the world of programming.
See slide [8-Stack].
Abstract Data Type -- applicative
Stack
functions
new : stack;
push : element * stack -> stack;
empty : stack -> boolean;
pop : stack -> stack;
top : stack -> element;
axioms
empty( new ) = true
empty( push(x,s) ) = false
top( push(x,s) ) = x
pop( push(x,s) ) = s
preconditions
pre: pop( s : stack ) = not empty(s)
pre: top( s : stack ) = not empty(s)
end
slide: The ADT Stack
Above, a stack has been specified by giving a signature
(consisting of the functions new, push, empty,
pop and top).
In addition to the axioms characterizing the behavior of the stack,
we have included two pre-conditions
to test whether the stack is empty in case pop
or top is applied.
The pre-conditions result in conditional
axioms for the operations pop and top.
Conditional axioms, however, do preserve
the initial algebra semantics.
The specification given above is a maximally
abstract description of the behavior of a stack.
Adding more implementation detail would disrupt
its nice applicative structure, without necessarily
resulting in different behavior (from a sufficiently
abstract perspective).
The behavior of elements of abstract data types
and objects is characterized by state changes.
State changes may affect the value delivered
by observers or methods.
Many state changes (such as the growing or shrinking of a
set, sequence or stack) really are nothing but applicative
transformations that may mathematically be described by
the input-output behavior of an appropriate function.
An example in which the value of an object
on some attribute is dependent on the history
of the operations applied to the object, instead of
the structure of the object itself (as in the case
of a stack) is the object account, as specified in
slide [8-account].
The example is taken from [Goguen].
Dynamic state changes -- objects
account
object account is
functions
bal : account -> money
methods
credit : account * money -> account
debit : account * money -> account
error
overdraw : money -> money
axioms
bal(new(A)) = 0
bal(credit(A,M)) = bal(A) + M
bal(debit(A,M)) = bal(A) - M if bal(A) >= M
error-axioms
bal(debit(A,M)) = overdraw(M) if bal(A) < M
end
slide: The algebraic specification of an account
An account object has one attribute function
(called bal) that delivers the amount of money
that is (still) in the account.
In addition, there are two method functions,
credit and debit that may respectively be used
to add or withdraw money from the account.
Finally, there is one special error function, overdraw,
that is used to define the result of balance
when there is not enough money left to grant
a debit request.
Error axioms are needed whenever
the proper axioms are stated conditionally,
that is contain an if expression.
The conditional parts of the axioms, including the
error axioms, must cover all possible cases.
Now, first look at the form of the axioms.
The axioms are specified as
$fn(method(Object,Args))\; =\; expr$
where fn specifies an attribute function
(bal in the case of account) and method a method
(either new, which is used to create new accounts,
credit or debit).
By convention, we assume that $method(Object,...)\; =\; Object$,
that is that a method function returns its first argument.
Applying a method thus results in redefining the value
of the function fn.
For example, invoking the method
$credit(acc,10)$ for the account acc
results in modifying the function bal
to deliver the value $bal(acc)\; +\; 10$ instead of simply $bal(acc)$.
In the example above, the axioms define the meaning of the function bal
with respect to the possible method applications.
It is not difficult to see
that these operations are of a non-applicative nature,
non-applicative in the sense that each time a method is
invoked the actual definition of bal is changed.
The change is necessary because, in contrast
to, for example, the functions employed in a
boolean algebra, the actual value of the account
may change in time in a completely arbitrary way.
A first order framework of (multi sorted) algebras
is not sufficiently strong to define the meaning of such changes.
What we need may be characterized as a multiple world semantics,
where each world corresponds to a possible state of the account.
As an alternative semantics we will also discuss
the interpretation of an object as an abstract machine,
which resembles an (initial) algebra with hidden sorts.
Multiple world semantics
From a semantic perspective, an object that changes its state
may be regarded as moving from one world to another,
when we see a world as representing a particular
state of affairs.
Take for example an arbitrary (say John's) account,
which has a balance of 500.
We may express this as $balance(accountJohn)\; =\; 500$.
Now, when we invoke the method credit, as
in $credit(accountJohn,\; 200)$,
then we expect the balance of the account to be raised
to 700.
In the language of the specification, this is expressed as
$bal(credit(accountJohn,200))\; =\; bal(accountJohn)\; +\; 200$
Semantically, the result is a state of affairs in which
$bal(accountJohn)\; =\; 700$.
In [Goguen] an operational interpretation is given
of a multiple world semantics by introducing a
database D (that stores the values of the
attribute functions of objects as first order terms)
which is transformed as the result of invoking
a method, into a new database $D\text{'}$ (that has an updated
value for the attribute function modified by the method).
The meaning of each database (or world) may be characterized
by an algebra and an interpretation as before.
The rules according to which transformations on a database
take place may be formulated as in slide [8-multiple].
Multiple world semantics -- inference rules
- $<<\; f(t\_1,...,t\_n),D\; >>\; ->\; <<\; v,\; D\; >>$
attribute
- $<<\; m(t\_1,...,t\_n),D\; >>\; ->\; <<\; t\_1,\; D\text{'}\; >>$
method
- $<<\; t\; ,\; D\; >>\; ->\; <<\; t\text{'},\; D\text{'}\; >>\; =>\; <<\; e(...,t,...),\; D\; >>\; ->\; <(...,t\text{'},...),\; d\text{'}>$
slide: The interpretation of change
The first rule (attribute) describes how attribute functions
are evaluated.
Whenever a function f with arguments
$t\_1,...,t\_n$
evaluates to a value (or expression) v, then the term $f(t\_1,...,t\_n)$
may be replaced by v without affecting the database D.
(We have simplified the treatment by omitting all aspects having
to do with matching and substitutions,
since such details are not needed to understand the process
of symbolic evaluation in a multiple world context.)
The next rule (method) describes the result of
evaluating a method. We assume that invoking the method
changes the database D into $D\text{'}$.
Recall that, by convention, a method returns its first
argument.
Finally, the last rule (composition) describes how we may glue all
this together.
No doubt, the reader needs an example to get a picture
of how this machinery actually works.
Example - a counter object
object ctr is ctr
function n : ctr -> nat
method incr : ctr -> ctr
axioms
n(new(C)) = 0
n(incr(C)) = n(C) + 1
end
slide: The object ctr
In slide [8-ctr], we have specified a simple object ctr with
an attribute function value
(delivering the value of the counter)
and a method function incr
(that may be used to increment the value of the counter).
Abstract evaluation
-[new]->
-[incr]->
-[incr]->
-[n]->
<2, { C[n:=2] }>
slide: An example of abstract evaluation
The end result of the evaluation depicted in slide [8-ctr-evl] is
the value 2 and a context (or database) in which the
value of the counter C is (also) 2.
The database is modified in each step
in which the method incr is applied.
When the attribute function value is evaluated
the database remains unchanged, since it is merely
consulted.
Objects as abstract machines
Multiple world semantics provide a very
powerful framework in which to define the meaning of object
specifications.
Yet, as illustrated above, the reasoning involved
has a very operational flavor and lacks the appealing
simplicity of the initial algebra semantics
given for abstract data types.
As an alternative, [Goguen] propose an interpretation
of objects (with dynamic state changes) as
abstract machines.
Recall that an initial algebra semantics defines
a model in which the elements are equivalence classes
representing the abstract values of the data type.
In effect, initial models are defined only up to
isomorphism (that is, structural equivalence with
similar models).
In essence, the framework of initial algebra semantics
allows us to abstract from the particular representation
of a data type, when assigning meaning to a specification.
From this perspective it does not matter, for example, whether
integers are represented in binary or decimal notation.
The notion of abstract machines generalizes
the notion of initial algebras in that it loosens the
requirement of (structural) isomorphism,
to allow for what we may call behavioral equivalence.
The idea underlying the notion of behavioral equivalence
is to make a distinction between visible sorts
and hidden sorts and to look only at the
visible sorts to determine whether two algebras $|A$ and $|B$
are behaviorally equivalent.
According to [Goguen], two algebras $|A$ and $|B$
are behaviorally equivalent if and only if the result
of evaluating any expression of a visible sort in $|A$
is the same as the result of evaluating that expression
in $|B$.
Now, an abstract machine
(in the sense of Goguen and Meseguer, 1986)
is simply the equivalence class of behaviorally equivalent
algebras, or in other words the maximally abstract
characterization of the visible behavior of
an abstract data type with (hidden) states.
The notion of abstract machines is of particular relevance
as a formal framework to characterize the (implementation)
refinement relation between objects.
For example, it is easy to determine that the behavior
of a stack implemented as a list is equivalent
to the behavior of a stack implemented by a pointer array,
whereas these objects are clearly not equivalent
from a structural point of view.
Moreover, the behavior of both conform (in an abstract sense)
with the behavior specified in an algebraic way.
Together, the notions of abstract machine and behavioral equivalence
provide a formalization of the notion of information hiding
in an algebraic setting.
In the chapters that follow we will look at alternative
formalisms to explain information hiding, polymorphism
and behavioral refinement.
object-oriented programming
Decomposition -- modules versus objects
subsections:
Abstract data types allow the programmer to define a complex
data structure and an associated collection of functions,
operating on that structure, in a consistent way.
Historically, the idea of data abstraction was originally
not type-oriented but arose from a more pragmatic concern with
information hiding and representation abstraction,
see [Parnas72b].
The first realization of the idea of data abstraction was
in the form of modules grouping a collection of functions
and allowing the actual representation
of the data structures underlying the values of
the (abstract) type domain to be hidden,
see also [Parnas72a].
In [Cook90], a comparison is made between the way in which
abstract
data types are realized traditionally (as modules)
and the way abstract data types
may be realized using object-oriented programming techniques.
According to [Cook90], these approaches must be regarded as
being orthogonal to one another and, being to some extent
complementary, deserve to be integrated in
a common framework.
After presenting an example highlighting the differences between
the two approaches, we will further explore these differences and
study the trade-offs with respect to possible extensions
and reuse of code.
Recall that abstract data types may be completely characterized
by a finite collection of generators and a number of
observer functions that are defined with respect to each possible
generator.
Following this idea, we may approach the specification of a data
abstraction by constructing a matrix
listing the generators column-wise and the observers
row-wise, which for each observer/generator pair
specifies
the value of the observer for that particular generator.
Incidentally, the definition of such a matrix allows us
to check
in an easy way
whether we have given a complete characterization of the data type.
Above, an example is given of the specification of a list,
with generators nil and cons, and observers empty, head
and tail.
(Note that we group the secondary producer tail with the observers.)
Now, the traditional way of realizing abstract data types
as modules may be characterized as operation oriented,
in the sense that the module realization of the type is organized
around the observers, resulting in a horizontal decomposition
of the matrix.
On the other hand, an object-oriented approach may be characterized
as data oriented, since the object realization of a type
is based on specifying a method interface for each
possible generator (sub)type,
resulting in a vertical decomposition of the matrix.
See slide [8-decomposition].
Note, however, that in practice, different generators need
not necessarily correspond to different (sub)classes.
Behavior may be subsumed in variables, as an object
cannot change its class/type.
Abstract interfaces
When choosing for the module realization of
the data abstraction list in C style, we are likely
to have an abstract functional interface as specified
in slide mod-face.
Modules -- a functional interface
ADT
typedef int element;
struct list;
extern list* nil();
extern list* cons(element e, list* l);
extern element head(list* l);
extern list* tail(list* l);
extern bool equal(list* l, list* m);
slide: Modules -- a functional interface
For convenience, the list has been restricted to
contain integer elements only.
However, at the expense of additional notation,
we could also easily define a generic list
by employing template functions as provided
by C++.
This is left as an exercise for the reader.
The interface of the abstract class list
given in slide [obj-face] has been defined
generically by employing templates.
Objects -- a method interface
OOP
template< class E >
class list {
public:
list() { }
virtual ~list() { }
virtual bool empty() = 0;
virtual E head() = 0;
virtual list* tail() = 0;
virtual bool operator==(list* m) = 0;
};
slide: Objects -- a method interface
Note that the equal function in the ADT
interface takes two arguments,
whereas the operator== function in the OOP
interface takes only one,
since the other is implicitly provided by the
object itself.
Representation and implementation
The realization of abstract data types as modules with
functions requires additional means to hide the
representation of the list type.
In contrast, with an object-oriented approach,
data hiding is effected by employing the encapsulation
facilities of classes.
Modules -- representation hiding
Modules provide a syntactic means to group related pieces of code
and to hide particular aspects of that code.
In slide [8-modules] an example is given of
the representation and the generator functions for
a list of integers.
Modules -- representation hiding
ADT
typedef int element;
enum { NIL, CONS };
struct list {
int tag;
element e;
list* next;
};
Generators
list* nil() { nil
list* l = new list; l->tag = NIL; return l;
}
list* cons( element e, list* l) { cons
list* x = new list;
x->tag = CONS; x->e = e; x->next = l;
return x;
}
slide: Data abstraction and modules
For implementing the list as a collection of
functions (ADT style), we employ a struct
with an explicit tag field, indicating whether
the list corresponds to nil or a cons.
The functions corresponding with the generators
create a new structure and initialize the tag
field.
In addition, the cons operator sets the
element and next field of the structure to
the arguments of cons.
The implementation of the observers is given
in slide [8-mod-impl].
Modules -- observers
ADT
int empty(list* lst) { return !lst || lst->tag == NIL; }
element head(list* l) { head
require( ! empty(l) );
return l->e;
}
list* tail(list* l) { tail
require( ! empty(l) );
return l->next;
}
bool equal(list* l, list* m) { equal
switch( l->tag) {
case NIL: return empty(m);
case CONS: return !empty(m) &&
head(l) == head(m) &&
tail(l) == tail(m);
}
}
slide: Modules -- observers
To determine whether the list is empty it suffices
to check whether the tag of the list is equal to
NIL.
For both head and tail the pre-condition is that
the list given as an argument is not empty.
If the pre-condition holds, the appropriate field
of the list structure is returned.
The equality operator, finally, performs an explicit
switch on the tag field, stating for each case
under what conditions the lists are equal.
Below, a program fragment is given that illustrates
the use of the list.
list* r = cons(1,cons(2,nil()));
while (!empty(r)) {
cout << head(r) << endl;
r = tail(r);
}
Note that both the generator functions nil and cons
take care of creating a new list structure.
Writing a function to destroy a list
is left as an exercise for the reader.
Objects -- method interface
The idea underlying an object-oriented decomposition
of the specification matrix of an abstract type
is to make a distinction between the (syntactic)
subtypes of the data type (corresponding with its generators)
and to specify for each subtype the value of all possible
observer functions.
(We speak of syntactic subtypes, following [Dahl92],
since these subtypes correspond to the generators
defining the value domain of the data type.
See [Dahl92] for a more extensive treatment.)
Method interface -- list
OOP
template< class E >
class nil : public list< E > { nil
public:
nil() {}
bool empty() { return 1; }
E head() { require( false ); return E(); }
list< E >* tail() { require( 0 ); return 0; }
bool operator==(list* m) { return m->empty(); }
};
template< class E >
class cons : public list< E > { cons
public:
cons(E e, list* l) : _e(e), next(l) {}
~cons() { delete next; }
bool empty() { return 0; }
E head() { return _e; }
list* tail() { return next; }
bool operator==(list* m);
protected:
E _e;
list* next;
};
slide: Data abstraction and objects
In the object realization in slide [8-objects],
each subtype element is defined as a
class inheriting from the list class.
For both generator types nil and cons the observer functions
are defined in a straightforward way.
Note that, in contrast to the ADT realization,
the distinction between the various cases
is implicit in the member function definitions
of the generator classes.
As an example of using the list classes consider
the program fragment below.
list<int>* r = new cons<int>(1, new cons<int>(2, new nil<int>));
while (! r->empty()) {
cout << r->head() << endl;
r = r->tail();
}
delete r;
For deleting a list we may employ the (virtual) destructor
of list, which recursively destroys the tail of a list.
Adding new generators
Abstract data types were developed with correctness and
security in mind, and not so much from a concern
with extensibility and reuse.
Nevertheless, it is interesting to compare the traditional
approach of realizing abstract data types
(employing modules) and the object-oriented approach (employing
objects as generator subtypes) with regard
to the ease with which a specification may be extended,
either by adding new generators or by adding new
observers.
Adding new generators -- representation
ADT
typedef int element;
enum { NIL, CONS, INTERVAL };
struct list {
int tag;
element e;
union { element z; list* next; };
};
Generator
list* interval( element x, element y ) {
list* l = new list;
if ( x <= y ) {
l->tag = INTERVAL;
l->e = x; l->z = y;
}
else l->tag = NIL;
return l;
}
slide: Modules and generators
Let us first look at what happens when we add
a new generator to a data type, such as
an interval list subtype, containing the integers
in the interval between two given integers.
For the module realization of the list,
adding an $interval(x,y)$ generator will result in an
extension of the (hidden) representation types
with an additional representation tag type INTERVAL
and the definition of a suitable generator function.
To represent the interval list type, we employ a
union to select between the next field,
which is used by the cons generator, and the z
field, which indicates the end of the interval.
Modifying the observers
ADT
element head(list* l) { head
require( ! empty(l) );
return l->e; // for both CONS and INTERVAL
}
list* tail(list* l) { tail
require( ! empty(l) );
switch( l->tag ) {
case CONS: return l->next;
case INTERVAL:
return interval((l->e)+1,l->z);
}
}
slide: Modifying the observers
Also, we need to modify the observer functions
by adding an appropriate case for the new interval
representation type, as pictured in slide [8-mod-xx].
Clearly, unless special constructs are provided,
the addition of a new generator case requires
disrupting the code implementing the given data type
manually, to extend the definition of the observers
with the new case.
In contrast, not surprisingly,
when we wish to add a new generator case
to the object realization of the list, we do not need to
disrupt the given code,
but we may simply add the definition of the generator
subtype as given in slide [8-oop-gen].
Adding new generators
OOP
class interval : public list<int> { interval
public:
interval(int x, int y) : _x(x), _y(y) { require( x <= y ); }
bool empty() { return 0; }
int head() { return _x; }
list< int >* tail() {
return (_x+1 <= _y)?
new interval(_x+1,_y):
new nil<int>;
}
bool operator==(list@lt;int>* m) {
return !m->empty() &&
_x == m->head() && tail() == m->tail();
}
protected:
int _x; int _y;
};
slide: Objects and generators
Adding a new generator subtype corresponds to
defining the realization for an abstract interface
class, which gives a method interface that its
subclasses must respect.
Observe, however, that we cannot exploit the
fact that a list is defined by an interval when
testing equality, since we cannot inspect the
type of the list as for the ADT implementation.
Adding new observers
Now, for the complementary case, what happens
when we add new observers to the specification of a
data type?
Somewhat surprisingly, the object-oriented approach
now seems to be at a disadvantage.
Since in a module realization of an abstract data type
the code is organized around observers, adding a new
observer function amounts simply to adding a new operation
with a case for each of the possible generator
types, as shown in slide [8-mod-obs].
Adding new observers
ADT
int length( list* l ) { length
switch( l->tag ) {
case NIL: return 0;
case CONS: return 1 + length(l->next);
case INTERVAL: return l->z - l->e + 1;
};
}
slide: Modules and observers
When we look at how we may extend a given object
realization of an abstract data type
with a new observer we are facing a problem.
The obvious solution is to modify the source
code and add the length function to the list
interface class and each of the generator classes.
This is, however, against the spirit of object
orientation and may not always be feasible.
Another, rather awkward solution,
is to extend the collection of
possible generator subtypes with a number of new
generator subtypes that explicitly incorporate the new
observer function.
However, this also means redefining the tail
function since it must deliver an instance
of a list with length class.
As a workaround, one may
define a function length
and an extended version of the
list template class supporting only the
length (observer) member function
as depicted in
slide [8-oop-obs].
Adding new observers
OOP
template< class E >
int length(list< E >* l) { length
return l->empty() ? 0 : 1 + length( l->tail() );
}
template< class E >
class listWL : public list<E> { listWL
public:
int length() { return ::length( this ); }
};
slide: Objects and observers
A program fragment illustrating the use of the
listWL class is given below.
list<int>* r = new cons<int>(1,new cons<int>(2,new interval(3,7)));
while (! r->empty()) {
cout << ((listWL< int >*)r)->length() << endl;
r = r->tail();
}
delete r;
Evidently, we need to
employ a cast whenever we wish to
apply the length observer function.
Hence, this seems not to be the right solution.
Alternatively, we may use the function length directly.
However, we are then forced to mix method
syntax of the form $ref->op(args)$ with function syntax
of the form $fun(ref,args)$, which may easily lead
to confusion.
Discussion
We may wonder why an object-oriented approach,
that is supposed to support extensibility, is
at a disadvantage here when compared to a more
traditional module-based approach.
As observed in [Cook90], the problem lies in the fact
that neither of the two approaches reflect
the full potential and flexibility of
the matrix specification of an abstract data type.
Each of the approaches represents a particular choice
with respect to the decomposition of the matrix, into
either an operations-oriented (horizontal) decomposition
or a data-oriented (vertical) decomposition.
The apparent misbehavior of an object realization
with respect to extending the specification with observer
functions explains why in some cases we prefer
the use of overloaded functions rather than methods,
since overloaded functions allow for implicit dispatching
to take place on multiple arguments,
whereas method dispatching behavior is determined only
by the type of the object.
However, it must be noted that the dispatching behavior
of overloaded functions in C++ is of a purely syntactic nature.
This means that we cannot exploit the information
specific for a class type as we can when using
virtual functions.
Hence, to employ this information we would be required
to write as many variants of overloaded functions
as there are combinations of argument
types.
Dynamic dispatching on multiple arguments is
supported by
multi-methods in CLOS,
see [Paepcke93].
According to [Cook90], the need for such methods
might be taken as a hint that objects
only partially realize the true potential of data abstraction.
object-oriented programming
Types versus classes
Types are primarily an aid in arriving at a consistent
system description.
Most (typed) object-oriented programming languages offer
support for types by employing classes as a device to define the
functionality of objects.
Classes, however, have originated from a far more pragmatic concern,
namely as a construct to enable the definition and creation of objects.
Concluding this chapter, we will reflect on the distinction between
types and classes, and discuss the role types and classes
play in reusing software through derivation by inheritance.
This discussion is meant to prepare the ground for a more formal
treatment to be given in the next chapter.
It closely follows the exposition given in [WZ88].
Types must primarily be understood as predicates to guide
the process of type checking,
whereas classes have come into being originally
as templates for object creation.
It is interesting to note how (and how easily) this
distinction may be obscured.
In practice, when compiling a program in Java or C++, the compiler will
notify the user of an error when a member function is called
that is not listed in the public interface of the objects class.
As another example, the runtime system of Smalltalk
will raise an exception, notifying the user of a dynamic type
error, when a method is invoked that is not defined in the object's
class or any of its superclasses.
Both kinds of errors have the flavor of a typing error,
yet they rely on different notions of typing and
are based on a radically different interpretation of classes as types.
To put types into perspective, we must ask ourselves what means we have
to indicate the type of an expression, including expressions
that somehow reference a class description.
In [WZ88], three attitudes towards typing are distinguished:
(1) typing may be regarded as an administrative aid to check
for simple typos and other administrative
errors, (2) typing may be regarded
as the ultimate solution to defining the behavior of a system,
or (3) typing may (pragmatically) be regarded as a consequence
of defining the behavior of an object.
See slide [8-classes].
Before continuing, the reader is invited to sort the various
programming languages discussed into the three slots mentioned.
Types versus classes
- types -- type checking predicates
- classes -- templates for object creation
Type specification
- syntactically -- signature
(under)
- semantically -- behavior
(right)
- pragmatically -- implementation
(over)
slide: Types and classes
Typing as an administrative aid is typically a task
for which we rely on a compiler to check
for possible errors.
Evidently, the notion of typing that a compiler employs is
of a rather syntactic nature.
Provided we have specified a signature correctly, we may trust
a compiler with the routine of checking for errors.
As languages that supports signature type checking we may (obviously)
mention Java and C++.
Evidently, we cannot trust the compiler to detect conceptual errors,
that is incomplete or ill-conceived definitions of the functionality of an object
or collections of objects.
Yet, ultimately we want to be able to specify the behavior of an
object in a formal way and to check mechanically for the adequacy
of this definition.
This ideal of semantic types underlies the design of Eiffel,
not so much the Eiffel type system as supported by the Eiffel
compiler, but the integration of assertions in the Eiffel language
and the notion of contracts as a design principle.
Pragmatically, we need to rely on runtime (consistency) checks
to detect erroneous behavior, since there are (theoretically rather severe)
limits on the extent to which we may verify behavioral properties
in advance.
(Nevertheless, see section [types-behavioral] for some attempts in
this direction.)
Modifications
- types -(predicate constraints)$->$ subtypes
- classes -(template modification)$->$ subclasses
Varieties of (compatible) modifications
- behaviorally -- algebraic, axiomatic
(type)
- signature -- type checking
(signature)
- name -- method search algorithm
(classes)
slide: Type modifications
Finally, we can take a far more pragmatic view towards
typing, by regarding the actual specification of a class as an implicit
characterization of the type of the instances of the class.
Actually, this is the way (not surprisingly, I would say)
types are dealt with in Smalltalk.
Each object in Smalltalk is typed, by virtue of being
an instance of a class.
Yet, a typing error may only be detected dynamically, as the result of
not responding to a message.
A distinction between perspectives on types
(respectively syntactic, behavioral and pragmatic)
may seem rather academic at first sight.
However, the differences are, so to speak, amplified when
studied in the context of type modifications,
as for example effected by inheritance.
[WZ88] make a distinction between three notions of
compatible modifications, corresponding to the three
perspectives on types, respectively
signature compatible modifications
(which require the preservation of the static signature),
behaviorally compatible modification
(which rely on a mathematical notion of definability for a type)
and name compatible modifications
(that rely on an operationally defined method search algorithm).
See slide [8-refinement].
Signature compatible modifications
The assumption underlying the notion of types as signatures
is that behavior is approximated by a (static) signature.
Now the question is: to what extent can we define semantics preserving
extensions to a given class or object?
Signature compatible modifications
- behavior is approximated by signature
Semantics preserving extensions
- horizontal -- Person = Citizen + { age : 0..120 }
- vertical -- Retiree = Person + { age : 65..120 }
Principle of substitutability
- an instance of a subtype can always be used in any context in which an instance of a supertype can be used
subsets are not subtypes
Retiree $\backslash not<\_\{subtype\}$ Person
Read-only substitutability
- subset subtypes, isomorphically embedded subtypes
slide: The principle of substitutability
When we conceive of an object as a record consisting of
(data and method) fields, we may think of two possible kinds of modifications.
We may think of a horizontal modification when adding a new field,
and similarly we may think of a modification as being vertical
when redefining or constraining a particular field.
For example, when we define Citizen as an entity with a name,
we may define (at the risk of being somewhat awkward)
a Person as a Citizen with an age and a Retiree as a Person
with an age that is restricted to the range 65..120.
The principle by which we may judge these extensions valid (or not)
may be characterized as the principle of substitutability,
which may be phrased as:
an instance of a subtype can always be used in any context in
which an instance of a supertype can be used.
Unfortunately, for the extension given here we have an easy
counterexample, showing that syntactic signature compatibility
is not sufficient.
Clearly, a Person is a supertype of Retiree
(we will demonstrate this more precisely in section [subtypes]).
Assume that we have a function
set_age : Person * Integer -> Void
that is defined as set_age(p,n) { p.age = n; }.
Now consider the following fragment of code:
Person* p = r; r refers to some Retiree
p->set_age(40);
where we employ object reference notation when calling $set\_age$.
Since we have assigned r (which is referring to a Retiree)
to p, we know that p now points to a Retiree,
and since a Retiree is a person we may apply
the function $set\_age$.
However, $set\_age$ sets the age of the Retiree to 40,
which gives (by common standards) a semantic error.
The lesson that we may draw from this is that being
a subset is no guarantee for being a subtype
as defined by the principle of substitutability.
However, we may characterize the relation between
a Retiree and a Person as being of a weaker kind,
namely read-only substitutability,
expressing that the (value of) the subtype may be used safely
everywhere an instance of the supertype is expected,
as long as it is not modified.
Read-only substitutability holds for a type that stands
in a subset relation to another type
or is embeddable (as a subset) into that type.
See slide [8-subst].
Behaviorally compatible modifications
If the subset relation is not a sufficient condition for
being in a subtype relation, what is?
To establish whether the (stronger) substitutability relation holds
we must take the possible functions associated with the types
into consideration as well.
First, let us consider what relations may exist between types.
Recall that semantically a type corresponds to
a set together with a collection of operations
that are defined for the set
and that the subtype relation corresponds to
the subset relation in the sense that (taking a type as a constraint)
the definition of a subtype involves adding a constraint and,
consequently,
a narrowing of the set of elements corresponding to the supertype.
Complete compatibility is what we achieve when the principle
of substitutability holds.
Theoretically, complete compatibility may be assured when the behavior of the
subtype fully complies with the behavior of the supertype.
Behavioral compatibility, however, is a quite demanding notion.
We will deal with it more extensively in chapter [refinement],
when discussing behavioral refinement.
Unfortunately, in practice we must often rely
on
the theoretically much weaker notion of
name compatibility.
Name compatible modifications
- operational semantics -- no extra compile/run-time checks
procedure search(name, module)
if name = action then do action
elsif inherited = nil
then undefined
else search(name, inherited)
slide: The inheritance search algorithm
Name compatible modifications
Name compatible modifications approximate behaviorally
compatible modifications in the sense that
substitutability is guaranteed, albeit not in a semantically
verifiable way.
Operationally, substitutability can be enforced
by requiring that each subclass (that we may characterize
as a pragmatic subtype) provides at least the operations
of its superclasses
(while giving a sensible result on all argument types
allowed by its superclasses).
Actually, name compatibility is an immediate consequence of
the overriding semantics of derivation by
inheritance, as reflected in the search algorithm underlying
method lookup.
See slide [8-search].
Although name compatible modifications are by far the most flexible,
from a theoretical point of view they are the least satisfying
since they do not allow for any theory formation concerning
the (desired) behavior of (the components of) the system
under development.
object-oriented programming
Summary
object-oriented programming
This chapter has presented an introduction
to the theoretical foundations of
abstract data types.
In particular, a characterization was
given of types as constraints.
1
- abstraction -- control and data
- abstract data types -- values in a semantic domain
- types as constraints -- mathematical models
slide: Section 8.1: Abstraction and types
In section 1,
we discussed the notion of abstraction
in programming languages and
distinguished between control and
data abstractions.
Abstract data types were characterized as values in some domain,
and we looked at the various ways in which
to define mathematical models
for types.
2
- signature -- producers and observers
- generator universe -- equivalence classes
- initial model -- no junk, no confusion
- objects -- multiple world semantics
slide: Section 8.2: Algebraic specification
In section 2,
we studied the algebraic specification
of abstract data types by means of
a signature characterizing producers
and observers.
We discussed the notions of equivalence
classes and initial models,
which consist of precisely the equivalence
classes that are needed.
,p>
Also, we looked at the interpretation of
objects as algebras, and we discussed
a multiple world semantics allowing for
dynamic state changes.
3
- data abstraction -- generators/observers matrix
- modules -- operation-oriented
- objects -- data-oriented
slide: Section 8.3: Decomposition -- modules versus objects
In section 3,
we looked at the various ways we may realize data abstractions
and we distinguished between a modular
approach, defining a collection of
operations, and a data-oriented approach,
employing objects.
4
- types -- syntactically, semantically, pragmatically
- compatible modifications -- type, signature, class
slide: Section 8.4: Types versus classes
Finally, in section 4, we discussed the differences
between a syntactic, semantic and operational
interpretation of types,
and how these viewpoints affect our
notion of refinement or compatible
modification.
object-oriented programming
- Characterize the differences between control
abstractions and data abstractions.
Explain how these two kinds of abstractions
may be embodied in programming language constructs.
- How can you model the meaning of abstract data types
in a mathematical way?
Do you know any alternative ways?
- Explain how types may affect object-oriented programming.
- Explain how you may characterize an abstract data type
by means of a matrix with generator columns and observer
rows.
What benefits does such an organization have?
- How would you characterize the differences between
the realization of abstract data types by modules
and by objects?
Discuss the trade-offs involved.
- How would you characterize the distinction
between types and classes?
Mention three ways of specifying types.
How are these kinds related to each other?
- How would you characterize behavior compatible
modifications?
What alternatives can you think of?
slide: Questions
object-oriented programming
There is a vast amount of literature on the algebraic
specification of abstract data types.
You may consult, for example, [Dahl92].
(C) Æliens
04/09/2009
You may not copy or print any of this material without explicit permission of the author or the publisher.
In case of other copyright issues, contact the author.