Menu Data Abstraction before clu data Abstraction in clu

Menu

• Data Abstraction before CLU

• Data Abstraction in CLU

• Reasoning about Data Abstractions

• Abstraction Functions
• Rep Invariants

What is a type?

• Last time: a set of values

• Today: an abstraction for decomposing a program that provides a set of operations

• Sets of values don’t work because you are tied to the representation

Data Abstraction in C/Pascal?

• User-defined types:

• typedef enum { red = 0, green, blue } color;
• typedef struct { int locx; int locy; } location;

• Type checking either:

• By structure (e.g., color dumb = 23)
• By name (maybe in Pascal, ambiguous)

• Only way to use type, is to access its representation; no restrictions on where you can do this.

Data Abstraction in BLISS?

• User specifies accessing algorithm for structure elements

• May modify either structure definition or algorithms without affecting the other

• structure array[i, j] = (.array + .i * 10 + .j)

• May define memory allocation routines

• But: only arrays, no typed elements

Data Abstraction in Simula67

• Define a class with hidden attributes (visible only in the class implementation) and protected attributes (visible in subclass implementations also)

• Unfortunately, not widely known:

• From Sweden
• Few Publications (mostly in Swedish), no language Report, no decent textbook until 1986
• Alan Kay learned about Simula by reading the source code, thinking it was an Algol compiler!
• Big influence on Smalltalk and C++; small influence on CLU

Providing Data Abstraction

• Type check by name

• Restrict what code can access the representation of a data type

• CLU, Alphard: only operations of the type
• Other (possibly) reasonable answers:
• C++: allow functions outside the type that are declared friends to access representation
• C with LCLint: in files and functions according to a naming convention, elsewhere when explicitly annotated
• [Stata97]: operations can access the only some of the representation

Data Abstraction in CLU

Black-box Interface

Parameterized Data Abstractions

• Don’t want to implement stringintmap, stringrealmap, intintmap, etc.

• Value Parameters:

• Don’t want to implement Factorial2 (), Factorial3 (), Factorial4 (), ...
• Implement Factorial (n: int)

• Type Parameters:

• Implement map[tkey: type, tval: type]

• Problem: how will we implement lookup if we don’t know anything about tkey?

Specification

• map = data type [tkey: type, tval: type] is create, insert, lookup

• Requires tkey has an operation

• equal: proctype (t, t) returns (bool)

• that is an equivalence relation on t.

• Operations

• create = proc () returns (map) effects Returns a new, empty map.

• insert = proc (s: map, k: tkey, val: tval)

• requires s has no key k’ such that tkey$equal (k, k’).

• modifies s

• effects lookup (spost. k) = val.

• lookup = proc (s: map, k: tkey) returns (tval)

• requires s has a key k’ in s such that tkey$equal (k, k’).

• effects Returns value associated with k in s.

Where Clauses

• map = cluster [tkey: type, tval: type] is create, insert, lookup

• where tkey has

Implementing Data Abstractions

• Need a concrete representation

Implementing map

• insert = proc (m: map, k: tkey, v: tval)

• % Better spec would remove requires

• % clause and signal exception if key

• % is already in the map.

• down (m).addh (pair${key: k, value: v})

• end insert

Printing maps

• map = cluster [tkey: type, tval] is ... unparse

• ...

• unparse = proc (m: map) returns (string)

• where

• tkey has unparse: proctype (tkey) returns (string)

• tval has unparse: proctype (tval) returns (string)

CLU: Special Types

• bool

• Language control structures (if, while) depend on type bool

• int, char, real, string, null

• Built-in language support for literals

• record, struct, variant, oneof, array, sequence

• Special constructor syntax T${ … }

• any

• Union of all possible types, use force to convert (with checking) to actual type

CLU Operators

• Assignment (:=)

• Always means sharing (recall immutable types)
• Types by name must match

• Everything else is syntactic sugar, all types can use:

• 3 + 2  int$add (3, 2)
• m1,m2: map[string,int] m1 + m2  map[string,int]$add (m1, m2)
• ai: array[int] ai[n] := ai[n-1] 
• array[int]$store (ai, n, array[int]$fetch (ai, n-1))

• Four exceptions: up, down, cand, cor

Questions?

• Next: Reasoning About Data Abstractions

Reasoning about Data Abstractions

• They are abstractions – need to invent a formal notation (A) for describing them

• They have representations – need to define a mapping from concrete representation to that formal notation

• Abstraction Function:

• A: rep  A

Describing maps

• A map can be described by a sequence of (key, value) pairs with unique keys:

• [ (key0, value0), (key1, value1), … ]

• such that if key = keyi the value associated with key is valuei .

Abstraction Function

• A: array [record [key: tkey, value: tval]]

•  [(key0, value0), (key1, value1), …]

• A(r) = [(r[rep$low(r)].key, r[rep$low(r)].value),

• (r[rep$low(r) + 1].key, r[rep$low(r)+1].value),

• ...

• (r[rep$high(r)].key, r[rep$high(r)].value)]

Rep Invariant

• “It better not!”

• I: rep  Boolean

Reasoning with Rep Invariants

• Prove by induction, for a datatype t:

• For each operation that creates new t: prove that returned reps r of returned t satisfies I(r)

• For each cluster operation: assume all t objects passed as parameters satisfy have reps r that satisfy I(r), prove they do at all cluster exit points.

• Argue that only cluster operations can alter the rep, so if you can prove invariant holds for all cluster operations, it must always hold.

What can go wrong?

• map = cluster [tkey: type, tval: type] is ...

• choose = proc (m: map)

• returns (record [key: tkey, value: tval])

• % requires m is not empty.

• % effects Returns a (key, value) pair in m.

• return (down (m)[rep$low (down(m))]

• end choose

Rep Exposure

• Can’t share mutable objects in data representations

• Sharing immutable objects is okay

• Could compiler prevent this?

• Yes, pretty easy

• Why doesn’t CLU compiler prevent this?

• Sometimes efficiency requires rep exposure
• e.g., create a map by passing in an array of pairs

The programming community must soon come to terms with the topics that they address, including: What are the qualitative and quantitave effects of strong type-checking? How do verification considerations affect language design? What abstraction mechanisms should languages provide? How can security of high-level languages be extended to real-time applications?

• The programming community must soon come to terms with the topics that they address, including: What are the qualitative and quantitave effects of strong type-checking? How do verification considerations affect language design? What abstraction mechanisms should languages provide? How can security of high-level languages be extended to real-time applications?

• Jim Horning, 1977 (from 6 March manifest)

Charge

• Read Stroustrup and Smalltalk papers before class Thursday

• Think about what Object-Oriented Programming really means – could Stroustrup and Ingalls really be writing about the same thing?

• Is CLU Object-Oriented? If not, would adding syntactic sugar make CLU object-oriented?