程序代写代做代考 data structure Java AVL case study Abstractions via Mathematical Models

Abstractions via Mathematical Models
EECS3311 M: Software Design Winter 2019
CHEN-WEI WANG

Motivating Problem: Complete Contracts
● Recall what we learned in the Complete Contracts lecture:
○ In post-condition , for each attribute , specify the relationship between its pre-state value and its post-state value.
○ Use the old keyword to refer to post-state values of expressions.
○ For a composite-structured attribute (e.g., arrays, linked-lists,
hash-tables, etc.), we should specify that after the update: 1. The intended change is present; and
2. The rest of the structure is unchanged .
● Let’s now revisit this technique by specifying a LIFO stack.
2 of 37

Motivating Problem: LIFO Stack (1)
● Let’s consider three different implementation strategies:
Stack Feature
Array
Linked List
Strategy 1
Strategy 2
Strategy 3
count
imp.count
top
imp[imp.count]
imp.first
imp.last
push(g)
imp.force(g, imp.count + 1)
imp.put front(g)
imp.extend(g)
pop
imp.list.remove tail (1)
list.start list.remove
imp.finish imp.remove
● Given that all strategies are meant for implementing the same ADT,willtheyhave identical contracts?
3 of 37

Motivating Problem: LIFO Stack (2.1)
class LIFO_STACK[G] create make feature {NONE} — Strategy 1: array
imp: ARRAY[G]
feature — Initialization
make do create imp.make_empty ensure imp.count = 0 end feature — Commands
push(g: G)
do imp.force(g, imp.count + 1) ensure
changed: imp[count]  g
unchanged: across 1 |..| count – 1 as i all
4 of 37
imp[i.item]  (old imp.deep_twin)[i.item] end
end
pop
do imp.remove_tail(1) ensure
changed: count = old count – 1 unchanged: across 1 |..| count as i all
end
imp[i.item]  (old imp.deep_twin)[i.item] end

Motivating Problem: LIFO Stack (2.2)
class LIFO_STACK[G] create make
feature {NONE} — Strategy 2: linked-list first item as top
imp: LINKED_LIST[G] feature — Initialization
make do create imp.make ensure imp.count = 0 end feature — Commands
push(g: G)
do imp.put_front(g) ensure
changed: imp.first  g
unchanged: across 2 |..| count as i all
5 of 37
imp[i.item]  (old imp.deep_twin)[i.item – 1] end
end
pop
do imp.start ; imp.remove ensure
changed: count = old count – 1 unchanged: across 1 |..| count as i all
end
imp[i.item]  (old imp.deep_twin)[i.item + 1] end

Motivating Problem: LIFO Stack (2.3)
class LIFO_STACK[G] create make
feature {NONE} — Strategy 3: linked-list last item as top
imp: LINKED_LIST[G] feature — Initialization
make do create imp.make ensure imp.count = 0 end feature — Commands
push(g: G)
do imp.extend(g) ensure
changed: imp.last  g
unchanged: across 1 |..| count – 1 as i all
6 of 37
imp[i.item]  (old imp.deep_twin)[i.item] end
end
pop
do imp.finish ; imp.remove ensure
changed: count = old count – 1 unchanged: across 1 |..| count as i all
end
imp[i.item]  (old imp.deep_twin)[i.item] end

Motivating Problem: LIFO Stack (3)



of all 3 versions of stack are . i.e., Not only the new item is pushed/popped, but also the
remaining part of the stack is unchanged.
But they violate the principle of information hiding :
Changing the secret, internal workings of data structures
should not affect any existing clients.
How so?
The private attribute imp is referenced in the postconditions ,
exposing the implementation strategy not relevant to clients:
● Topofstackmaybe , ,or .
● Remainingpartofstackmaybe or
.
⇒ Changing the implementation strategy from one to another will
also .
⇒ This also violates the .
Postconditions
complete
7 of 37
imp[count]
imp.first
across 1 |..| count – 1
imp.last
across 2 |..| count
change the contracts for all features
Single Choice Principle

Math Models: Command vs Query
○ Use MATHMODELS library to create math objects (SET, REL, SEQ). ○ State-changing commands: Implement an
8 of 37
class LIFO_STACK[G -> attached ANY] create make feature {NONE} — Implementation
imp: LINKED_LIST[G]
feature — Abstraction function of the stack ADT
model: SEQ[G]
do create Result.make_empty
across imp as cursor loop Result.append(cursor.item) end end
○ Side-effect-free queries: Write Complete Contracts
class LIFO_STACK[G -> attached ANY] create make feature — Abstraction function of the stack ADT
model: SEQ[G] feature — Commands
push (g: G)
ensure model  (old model.deep_twin).appended(g) end
Abstraction Function

Implementing an Abstraction Function (1)
class LIFO_STACK[G -> attached ANY] create make feature {NONE} — Implementation Strategy 1
imp: ARRAY[G]
feature — Abstraction function of the stack ADT model: SEQ[G]
do create Result.make from array (imp) ensure
counts: imp.count = Result.count
contents: across 1 |..| Result.count as i all
Result[i.item]  imp[i.item]
end
feature — Commands
make do create imp.make empty ensure model.count = 0 end push (g: G) do imp.force(g, imp.count + 1)
ensure pushed: model  (old model.deep twin).appended(g) end pop do imp.remove tail(1)
ensure popped: model  (old model.deep twin).front end end
9 of 37

Abstracting ADTs as Math Models (1)
old model: SEQ[G]
model ~ (old model.deep_twin).appended(g)
model: SEQ[G]
abstraction function
convert the current array convert the current array into a math sequence into a math sequence
old imp: ARRAY[G]
imp.force(g, imp.count + 1)
imp: ARRAY[G]
Strategy 1
● : Convert the implementation array to its corresponding model sequence.

for the feature remains the same:
10 of 37
‘push(g: G)’ feature of LIFO_STACK ADT
public (client’s view)
Abstraction function
abstraction function
private/hidden (implementor’s view)
Contract
put(g: G)
model  (old model.deep_twin).appended(g)

Implementing an Abstraction Function (2)
class LIFO_STACK[G -> attached ANY] create make
feature {NONE} — Implementation Strategy 2 (first as top)
imp: LINKED LIST[G]
feature — Abstraction function of the stack ADT model: SEQ[G]
do create Result.make_empty
across imp as cursor loop Result.prepend(cursor.item) end
ensure
counts: imp.count = Result.count
contents: across 1 |..| Result.count as i all
Result[i.item]  imp[count – i.item + 1]
end
feature — Commands
make do create imp.make ensure model.count = 0 end push (g: G) do imp.put front(g)
ensure pushed: model  (old model.deep twin).appended(g) end pop do imp.start ; imp.remove
ensure popped: model  (old model.deep twin).front end end
11 of 37

Abstracting ADTs as Math Models (2)
old model: SEQ[G]
model ~ (old model.deep_twin).appended(g)
model: SEQ[G]
abstraction function
convert the current liked list convert the current linked list into a math sequence into a math sequence
old imp: LINKED_LIST[G]
imp.put_front(g)
imp: LINKED_LIST[G]
Strategy 2
● : Convert the implementation list (first item is top) to its corresponding model sequence.

for the feature remains the same:
12 of 37
‘push(g: G)’ feature of LIFO_STACK ADT
public (client’s view)
Abstraction function
abstraction function
private/hidden (implementor’s view)
Contract
put(g: G)
model  (old model.deep_twin).appended(g)

Implementing an Abstraction Function (3)
class LIFO_STACK[G -> attached ANY] create make
feature {NONE} — Implementation Strategy 3 (last as top)
imp: LINKED LIST[G]
feature — Abstraction function of the stack ADT model: SEQ[G]
do create Result.make_empty
across imp as cursor loop Result.append(cursor.item) end
ensure
counts: imp.count = Result.count
contents: across 1 |..| Result.count as i all
Result[i.item]  imp[i.item]
end
feature — Commands
make do create imp.make ensure model.count = 0 end push (g: G) do imp.extend(g)
ensure pushed: model  (old model.deep twin).appended(g) end pop do imp.finish ; imp.remove
ensure popped: model  (old model.deep twin).front end end
13 of 37

Abstracting ADTs as Math Models (3)
old model: SEQ[G]
model ~ (old model.deep_twin).appended(g)
model: SEQ[G]
abstraction function
convert the current liked list convert the current linked list into a math sequence into a math sequence
old imp: LINKED_LIST[G]
imp.extend(g)
imp: LINKED_LIST[G]
Strategy 3
● : Convert the implementation list (last item is top) to its corresponding model sequence.

for the feature remains the same:
14 of 37
‘push(g: G)’ feature of LIFO_STACK ADT
public (client’s view)
Abstraction function
abstraction function
private/hidden (implementor’s view)
Contract
put(g: G)
model  (old model.deep_twin).appended(g)

Solution: Abstracting ADTs as Math Models
● Writing contracts in terms of implementation attributes (arrays, LL’s, hash tables, etc.) violates information hiding principle.
● Instead:
○ For each ADT, create an abstraction via a mathematical model.
e.g., Abstract a LIFO STACK as a mathematical .
○ For each ADT, define an abstraction function (i.e., a query)
whose return type is a kind of mathematical model.
e.g., Convert implementation array to mathematical sequence
○ Write contracts in terms of the abstract math model.
e.g., When pushing an item g onto the stack, specify it as
appending g into its model sequence.
○ Upon changing the implementation:
● Nochangeonwhattheabstractionis,hencenochangeoncontracts. ● Onlychangehowtheabstractionisconstructed,hencechangeson
the body of the abstraction function.
e.g., Convert implementation linked-list to mathematical sequence  The Single Choice Principle is obeyed.
sequence
15 of 37

Math Review: Set Definitions and Membership
● A set is a collection of objects.
○ Objects in a set are called its elements or members.
○ Order in which elements are arranged does not matter. ○ An element can appear at most once in the set.
● We may define a set using:
○ Set Enumeration: Explicitly list all members in a set.
e.g., {1, 3, 5, 7, 9}
○ Set Comprehension: Implicitly specify the condition that all
members satisfy.
e.g.,{x ∣1≤x ≤10∧x is an odd number}
● An empty set (denoted as {} or ∅) has no members.
● We may check if an element is a member of a set:
e.g., 5 ∈ {1, 3, 5, 7, 9}
e.g.,4∈/{x ∣x ≤1≤10,x is an odd number}
● The number of elements in a set is called its cardinality.
e.g.,∣∅∣=0,∣{x ∣x ≤1≤10,x is an odd number}∣=5 16 of 37
[true] [true]

Math Review: Set Relations
Given two sets S1 and S2:
● S1 isasubset ofS2 ifeverymemberofS1 isamemberofS2.
S1 ⊆ S2 ⇐⇒ (∀x ● x ∈ S1 ⇒ x ∈ S2)
● S1 and S2 are equal iff they are the subset of each other.
S1=S2 ⇐⇒S1⊆S2∧S2⊆S1
● S1 is a proper subset of S2 if it is a strictly smaller subset. S1⊂S2 ⇐⇒S1⊆S2∧∣S1∣<∣S2∣ 17 of 37 Math Review: Set Operations Given two sets S1 and S2: ● Union of S1 and S2 is a set whose members are in either. S1 ∪ S2 = {x ∣ x ∈ S1 ∨ x ∈ S2} ● Intersection of S1 and S2 is a set whose members are in both. S1 ∩ S2 = {x ∣ x ∈ S1 ∧ x ∈ S2} ● Difference of S1 and S2 is a set whose members are in S1 but not S2. 18 of 37 S 1 ∖ S 2 = { x ∣ x ∈ S 1 ∧ x ∈/ S 2 } Math Review: Power Sets The power set of a set S is a set of all S’ subsets. P(S) = {s ∣ s ⊆ S} The power set contains subsets of cardinalities 0, 1, 2, . . . , ∣S∣. e.g., P({1, 2, 3}) is a set of sets, where each member set s has cardinality 0, 1, 2, or 3: ⎧⎪ ⎪ ∅ , ⎫⎪ ⎪ ⎪⎪ ⎪ {1}, {2}, {3}, ⎪ ⎨⎪ {1,2}, {2,3}, {3,1}, ⎬⎪ ⎪⎩ {1,2,3} ⎪⎭ 19 of 37 Math Review: Set of Tuples Given n sets S1, S2, . . . , Sn, a cross product of theses sets is a set of n-tuples. Each n-tuple (e1, e2, . . . , en) contains n elements, each of which a member of the corresponding set. S1×S2×⋅⋅⋅×Sn ={(e1,e2,...,en)∣ei ∈Si ∧1≤i≤n} e.g., {a,b}×{2,4}×{$,&} is a set of triples: {a,b}×{2,4}×{$,&} = {(e1,e2,e3)∣e1 ∈{a,b}∧e2 ∈{2,4}∧e3 ∈{$,&}} {(a,2,$),(a,2,&),(a,4,$),(a,4,&), (b,2,$),(b,2,&),(b,4,$),(b,4,&)} 20 of 37 = Math Models: Relations (1) ● A relation is a collection of mappings, each being an ordered pair that maps a member of set S to a member of set T. e.g., Say S = {1,2,3} and T = {a,b} ○ ∅ is an empty relation. ○ S × T is a relation (say r1) that maps from each member of S to each member in T : {(1, a), (1, b), (2, a), (2, b), (3, a), (3, b)} ○ {(x,y)∶S×T ∣x ≠1}isarelation(sayr2)thatmapsonlysome members in S to every member in T : {(2, a), (2, b), (3, a), (3, b)}. ● Given a relation r: ○ Domain of r is the set of S members that r maps from. dom(r ) = {s ∶ S ∣ (∃t ● (s, t ) ∈ r )} e.g., dom(r1 ) = {1, 2, 3}, dom(r2 ) = {2, 3} ○ Range of r is the set of T members that r maps to. ran(r)={t∶T ∣(∃s●(s,t)∈r)} e.g., ran(r1) = {a, b} = ran(r2) 21 of 37 Math Models: Relations (2) ● We use the power set operator to express the set of all possible relations on S and T : P(S × T ) ● To declare a relation variable r, we use the colon (:) symbol to mean set membership: ● Or alternatively, we write: r ∶ P(S × T ) where the set S ↔ T is synonymous to the set P(S × T) 22 of 37 r∶S↔T Math Models: Relations (3.1) ● ● ● Say r = {(a,1),(b,2),(c,3),(a,4),(b,5),(c,6),(d,1),(e,2),(f,3)} : set of first-elements from r ○ r.domain={d ∣(d,r)∈r } ○ e.g., r.domain = {a,b,c,d,e,f} : set of second-elements from r ○ r.range={r ∣(d,r)∈r } ○ e.g.,r.range={1,2,3,4,5,6} : a relation like r except elements are in reverse order ○ r.inverse={(r,d)∣(d,r)∈r } r.domain r.range r.inverse ○ e.g., r.inverse = {(1,a),(2,b),(3,c),(4,a),(5,b),(6,c),(1,d),(2,e),(3,f)} 23 of 37 Math Models: Relations (3.2) ● ● ● ● Say r = {(a,1),(b,2),(c,3),(a,4),(b,5),(c,6),(d,1),(e,2),(f,3)} : sub-relation of r with domain ds. ○ r.domainrestricted(ds)={(d,r)∣(d,r)∈r∧d∈ds} ○ e.g.,r.domainrestricted({a,b})={(a,1),(b,2),(a,4),(b,5)} : sub-relation of r with domain not ds. ○ r.domainsubtracted(ds)={(d,r)∣(d,r)∈r∧d∈/ds} ○ e.g.,r.domainsubtracted({a,b})={(c,6),(d,1),(e,2),(f,3)} : sub-relation of r with range rs. ○ r.rangerestricted(rs)={(d,r)∣(d,r)∈r∧r∈rs} ○ e.g.,r.rangerestricted({1,2})={(a,1),(b,2),(d,1),(e,2)} : sub-relation of r with range not ds. ○ r.rangesubtracted(rs)={(d,r)∣(d,r)∈r∧r∈/rs} r.domain restricted(ds) r.domain subtracted(ds) r.range restricted(rs) r.range subtracted(ds) ○ e.g.,r.rangesubtracted({1,2})={(c,3),(a,4),(b,5),(c,6)} 24 of 37 Math Models: Relations (3.3) ● Say r = {(a,1),(b,2),(c,3),(a,4),(b,5),(c,6),(d,1),(e,2),(f,3)} : a relation which agrees on r outside domain of t.domain, and agrees on t within domain of t.domain ○ r.overridden(t)=t∪r.domainsubtracted(t.domain) ○ r .overridden({(a, 3), (c, 4)}) 􏰀􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰂􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰁 t = {(a,3),(c,4)}∪{(b,2),(b,5),(d,1),(e,2),(f,3)} 􏰀􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰂􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰁 􏰀􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰂􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰁 25 of 37 r.overridden(t) t r.domain subtracted(t.domain) 􏰀􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰂􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰁 {a,c} = {(a,3),(c,4),(b,2),(b,5),(d,1),(e,2),(f,3)} Math Review: Functions (1) A function f on sets S and T is a specialized form of relation: it is forbidden for a member of S to map to more than one members of T . ∀s ∶ S; t1 ∶ T ; t2 ∶ T ● (s, t1) ∈ f ∧ (s, t2) ∈ f ⇒ t1 = t2 e.g., Say S = {1, 2, 3} and T = {a, b}, which of the following relations are also functions? ○ S×T [No] ○ (S×T)−{(x,y)∣(x,y)∈S×T∧x=1} [No] ○ {(1,a),(2,b),(3,a)} [Yes] ○ {(1,a),(2,b)} [Yes] 26 of 37 Math Review: Functions (2) ● We use set comprehension to express the set of all possible functions on S and T as those relations that satisfy the functional property : {r ∶ S ↔ T ∣ (∀s ∶ S; t1 ∶ T ; t2 ∶ T ● (s, t1) ∈ r ∧ (s, t2) ∈ r ⇒ t1 = t2)} ● This set (of possible functions) is a subset of the set (of possible relations): P(S × T ) and S ↔ T . ● We abbreviate this set of possible functions as S → T and use it to declare a function variable f : f∶S→T 27 of 37 Math Review: Functions (3.1) Given a function f ∶ S → T : ● f is injective (or an injection) if f does not map a member of S to more than one members of T . f is injective ⇐⇒ (∀s1 ∶S;s2 ∶S;t ∶T ●(s1,t)∈r ∧(s2,t)∈r ⇒s1 =s2) e.g., Considering an array as a function from integers to objects, being injective means that the array does not contain any duplicates. ● f is surjective (or a surjection) if f maps to all members of T . f is surjective ⇐⇒ ran(f ) = T ● f is bijective (or a bijection) if f is both injective and surjective. 28 of 37 Math Review: Functions (3.2) 29 of 37 Math Models: Command-Query Separation Command domain restrict domain restrict by domain subtract domain subtract by range restrict range restrict by range subtract range subtract by override override by Query domain restricted domain restricted by domain subtracted domain subtracted by range restricted range restricted by range subtracted range subtracted by overridden overridden by Say r = {(a,1),(b,2),(c,3),(a,4),(b,5),(c,6),(d,1),(e,2),(f,3)} ● Commands modify the context relation objects. changes r to {(a, 1), (a, 4)} ● Queries return new relations without modifying context objects. returns {(a, 1), (a, 4)} with r untouched 30 of 37 r.domain restrict({a}) r.domain restricted({a}) Math Models: Example Test test_rel: BOOLEAN local r, t: REL[STRING, INTEGER] ds: SET[STRING] do create r.make_from_tuple_array ( <<["a", 1], ["b", 2], ["c", 3], ["a", 4], ["b", 5], ["c", 6], ["d", 1], ["e", 2], ["f", 3]>>)
create ds.make_from_array (<<"a">>)
— r is not changed by the query ‘domain_subtracted’ t := r.domain subtracted (ds)
Result :=
t / r and not t.domain.has (“a”) and r.domain.has (“a”) check Result end
— r is changed by the command ‘domain_subtract’
r.domain subtract (ds)
Result :=
t  r and not t.domain.has (“a”) and not r.domain.has (“a”)
end
31 of 37

Case Study: A Birthday Book
● A birthday book stores a collection of entries, where each entry is a pair of a person’s name and their birthday.
● No two entries stored in the book are allowed to have the same name.
● Each birthday is characterized by a month and a day.
● A birthday book is first created to contain an empty collection of entires.
● Given a birthday book, we may:
○ Inquire about the number of entries currently stored in the book
○ Add a new entry by supplying its name and the associated birthday ○ Remove the entry associated with a particular person
○ Find the birthday of a particular person
○ Get a reminder list of names of people who share a given birthday
32 of 37

Birthday Book: Decisions
● Design Decision ○ Classes
○ Client Supplier vs. Inheritance ○ Mathematical Model?
○ Contracts
● Implementation Decision
○ Two linear structures (e.g., arrays, lists)
○ A balanced search tree (e.g., AVL tree) ○ A hash table
[ e.g., REL or FUN ]
[ O(n) ] [ O(log ⋅ n) ] [ O(1) ]
● Implement an abstract function that maps implementation to the math model.
33 of 37

Birthday Book: Design
BIRTHDAY_BOOK
model: FUN[NAME, BIRTHDAY] ­­ abstraction function
count: INTEGER
­­ number of entries
put(n: NAME; d: BIRTHDAY)
ensure
model_operation: model ~ (old model.deep_twin).overriden_by ([n,d]) ­­ infix symbol for override operator: @<+ remind(d: BIRTHDAY): ARRAY[NAME] ensure nothing_changed: model ~ (old model.deep_twin) same_counts: Result.count = (model.range_restricted_by(d)).count same_contents: ∀ name ∈ (model.range_restricted_by(d)).domain: name ∈ Result ­­ infix symbol for range restriction: model @> (d)
invariant:
consistent_book_and_model_counts: count = model.count
model: FUN[NAME, ..]
BIRTHDAY
day: INTEGER month: INTEGER
invariant
1 ≤ month ≤ 12 1 ≤ day ≤ 31
NAME item: STRING
invariant
item[1] ∈ A..Z
34 of 37
remind: ARRAY[NAME]

Birthday Book: Implementation
35 of 37
BIRTHDAY_BOOK
model: FUN[NAME, BIRTHDAY] ­­ abstraction function
do
­­ promote hashtable to function
ensure
same_counts: Result.count = implementation.count
same_contents: ∀ [name, date] ∈ Result: [name, date] ∈ implementation
end
put(n: NAME; d: BIRTHDAY)
do
­­ implement using hashtable
ensure
model_operation: model ~ (old model.deep_twin) @<+ [n,d] end remind(d: BIRTHDAY): ARRAY[NAME] do ­­ implement using hashtable ensure nothing_changed: model ~ (old model.deep_twin) same_counts: Result.count = (model @> d).count same_contents: ∀ name ∈ (model @> d).domain: name ∈ Result
end
count: INTEGER ­­ number of names
feature {NONE}
implementation: HASH_TABLE[BIRTHDAY, NAME]
invariant:
consistent_book_and_model_counts: count = model.count consistent_book_and_imp_counts: count = implementation.count
model: FUN[NAME, ..]
BIRTHDAY
day: INTEGER month: INTEGER
invariant
1 ≤ month ≤ 12 1 ≤ day ≤ 31
* HASHABLE
NAME item: STRING
invariant
item[1] ∈ A..Z
remind: ARRAY[NAME]

Beyond this lecture . . .
● Familiarize yourself with the features of classes SEQ, REL, FUN,
and SET for the lab test.
● Play with the source code of the Birthday Book example: https://github.com/yuselg/eiffel/tree/master/snippets/ birthday- book.
● Exercise:
○ Consider an alternative implementation using two linear structures
(e.g., here in Java).
○ Create another LINEAR BIRTHDAY BOOK class and modify the
implementation of abstraction function accordingly. Do all contracts still pass?
36 of 37

Index (1)
Motivating Problem: Complete Contracts Motivating Problem: LIFO Stack (1) Motivating Problem: LIFO Stack (2.1) Motivating Problem: LIFO Stack (2.2) Motivating Problem: LIFO Stack (2.3) Motivating Problem: LIFO Stack (3)
Math Models: Command vs Query Implementing an Abstraction Function (1) Abstracting ADTs as Math Models (1) Implementing an Abstraction Function (2) Abstracting ADTs as Math Models (2) Implementing an Abstraction Function (3) Abstracting ADTs as Math Models (3)
Solution: Abstracting ADTs as Math Models
37 of 37

Index (2)
Math Review: Set Definitions and Membership Math Review: Set Relations
Math Review: Set Operations
Math Review: Power Sets
Math Review: Set of Tuples Math Models: Relations (1) Math Models: Relations (2) Math Models: Relations (3.1) Math Models: Relations (3.2) Math Models: Relations (3.3) Math Review: Functions (1) Math Review: Functions (2) Math Review: Functions (3.1)
Math Review: Functions (3.2)
38 of 37

Index (3)
Math Models: Command-Query Separation
Math Models: Example Test Case Study: A Birthday Book Birthday Book: Decisions Birthday Book: Design Birthday Book: Implementation
Beyond this lecture . . . 39 of 37