Key Points:

Describing Objects - ADTs

Formal Specification of ADTs

Classification of ADT functions

Reference:

O-O Software Construction by Meyer - Ch.4, 7, 10

Principles of O-O Software Development by Anton Eliens - Ch.8

O-O Programming in Eiffel by Thomas & Weedon - Ch. 3, 8

Abstractions in Programming Languages

- Control abstractions & Data

abstractions

Mathematical models - Types as constraints

- Algebra - set oriented

- second order lambda calculus -

polymorphic types

- constructive mathematics -

formulas as types

Objectives of a typing system & OO

- packaging, flexibility, inheritance,

reuse, binding

- reusability, extendibility & ADTs

Algebraic specification

- Signatures - Generators and

observers

- Equations - specifying constraints

- Objects as algebras

. Multiple world semantics

. Objects as abstract machines

Decomposition - Modules versus Objects

- Data abstraction - Generators/Observers Matrix

- Modules - Operation-oriented

- Objects - Data-oriented

Types versus Classes

- Types - type checking predicates

- Classes - templates for object creation

- Type specification - syntactic -

signature, semantic - behaviour,

pragmatic implementation

- Modification

- type (predicate constraints) -

subtyping,

- class (template modification) -

subclassing

- behaviourally - algebraic,

axiomatic (type)

- signature - type checking

(signature)

- name - method search algorithm

(classes)

Semantics of ADTs

- Axiomatic approach versus

Constructive approach

- Preconditions, postconditions &

underlying models

- Client Supplier relationship

ABSTRACT DATA TYPE (Definition)

- Name of the type

- Signature of the functions

- preconditions that constrain the

applicability of these functions

- axioms that express their properties

Eg. STACK as an ADT:

TYPES

STACK [X]

FUNCTIONS

empty: STACK [X] -> BOOLEAN

new: -> STACK [X]

push: X x STACK [X] -> STACK [X]

pop: STACK [X] -/-> STACK [X]

top: STACK [X] -/-> X

PRECONDITIONS

pre pop (s: STACK [X]) =

(not empty (s))

pre top (s: STACK [X]) =

(not empty (s))

AXIOMS

For all x: X, s: STACK [X]:

empty (new ( ))

not empty (push (x, s))

top (push (x, s)) = x

pop (push (x, s)) = s

CLASSIFICATION OF ADT FUNCTIONS

3 kinds of functions may appear in an ADT spec.

- Accessor e.g. empty & top

- Transformer e.g. push & pop

- Constructor e.g. new

HOW TO TRANSPOSE THE AXIOMS OF ADT SPECIFICATIONS TO A CLASS?

- Preconditions of spec reappear as

routine preconditions

- Axioms involving transformer

functions reappear as postconditions

of the corresponding procedures

- Axioms with only accessor functions

reappear as postconditions of the

corresponding functions or as clauses

of the class invariant.

- Axioms involving constructor

functions reappear in the postcondition

of the Make procedure.

THE ALGEBRAIC SPECIFICATION

OF

AN ACCOUNT

object account is

functions

bal: account -> money

methods

credit: account x money -> account

debit : account x 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

The axioms are specified above as func. (Method(Object,args)) = expr

where func. specifies the attribute

function (bal) & method either

new, credit or debit.

( Here the value of the account object on some attribute is dependent on the

history of operations applied to that object, instead of the structure of the object itself -

compare it to stack eg.)