COMP3141 – Data Invariants, Abstraction and Refinement
Data Invariants and ADTs Validation Data Refinement Administrivia
Software System Design and Implementation
Data Invariants, Abstraction and Refinement
Christine Rizkallah
UNSW Sydney
Term 2 2021
1
Data Invariants and ADTs Validation Data Refinement Administrivia
Motivation
We’ve already seen how to prove and test correctness properties of our programs.
How do we come up with correctness properties in the first place?
2
Data Invariants and ADTs Validation Data Refinement Administrivia
Structure of a Module
A Haskell program will usually be made up of many modules, each of which exports
one or more data types.
Typically a module for a data type X will also provide a set of functions, called
operations, on X.
• to construct the data type: c :: · · · → X
• to query information from the data type: q :: X→ · · ·
• to update the data type: u :: · · · X→ X
A lot of software can be designed with this structure.
Example (Data Types)
A dictionary data type, with empty, insert and lookup.
3
Data Invariants and ADTs Validation Data Refinement Administrivia
Data Invariants
One source of properties is data invariants.
Data Invariants
Data invariants are properties that pertain to a particular data type.
Whenever we use operations on that data type, we want to know that our data
invariants are maintained.
Example
That a list of words in a dictionary is always in sorted order
That a binary tree satisfies the search tree properties.
That a date value will never be invalid (e.g. 31/13/2019).
4
Data Invariants and ADTs Validation Data Refinement Administrivia
Properties for Data Invariants
For a given data type X, we define a wellformedness predicate
wf :: X→ Bool
For a given value x :: X, wf x returns true iff our data invariants hold for the value x .
Properties
For each operation, if all input values of type X satisfy wf, all output values will satisfy
wf.
In other words, for each constructor operation c :: · · · → X, we must show wf (c · · · ),
and for each update operation u :: X→ X we must show wf x =⇒ wf(u x)
Demo: Dictionary example, sorted order.
5
Data Invariants and ADTs Validation Data Refinement Administrivia
Stopping External Tampering
Even with our sorted dictionary example, there’s nothing to stop a malicious or clueless
programmer from going in and mucking up our data invariants.
Example
The malicious programmer could just add a word directly to the dictionary, unsorted,
bypassing our carefully written insert function.
We want to prevent this sort of thing from happening.
6
Data Invariants and ADTs Validation Data Refinement Administrivia
Abstract Data Types
An abstract data type (ADT) is a data type where the implementation details of the
type and its associated operations are hidden.
newtype Dict
type Word = String
type Definition = String
emptyDict :: Dict
insertWord :: Word -> Definition -> Dict -> Dict
lookup :: Word -> Dict -> Maybe Definition
If we don’t have access to the implementation of Dict, then we can only access it via
the provided operations, which we know preserve our data invariants. Thus, our data
invariants cannot be violated if this module is correct.
Demo: In Haskell, we make ADTs with module headers.
7
Data Invariants and ADTs Validation Data Refinement Administrivia
Abstract Data Types
An abstract data type (ADT) is a data type where the implementation details of the
type and its associated operations are hidden.
newtype Dict
type Word = String
type Definition = String
emptyDict :: Dict
insertWord :: Word -> Definition -> Dict -> Dict
lookup :: Word -> Dict -> Maybe Definition
If we don’t have access to the implementation of Dict, then we can only access it via
the provided operations, which we know preserve our data invariants. Thus, our data
invariants cannot be violated if this module is correct.
Demo: In Haskell, we make ADTs with module headers.
8
Data Invariants and ADTs Validation Data Refinement Administrivia
Abstract Data Types
An abstract data type (ADT) is a data type where the implementation details of the
type and its associated operations are hidden.
newtype Dict
type Word = String
type Definition = String
emptyDict :: Dict
insertWord :: Word -> Definition -> Dict -> Dict
lookup :: Word -> Dict -> Maybe Definition
If we don’t have access to the implementation of Dict, then we can only access it via
the provided operations, which we know preserve our data invariants. Thus, our data
invariants cannot be violated if this module is correct.
Demo: In Haskell, we make ADTs with module headers.
9
Data Invariants and ADTs Validation Data Refinement Administrivia
Abstract? Data Types
In general, abstraction is the process of eliminating detail.
The inverse of abstraction is called refinement.
Abstract data types like the dictionary above are abstract in the sense that their
implementation details are hidden, and we no longer have to reason about them on the
level of implementation.
10
Data Invariants and ADTs Validation Data Refinement Administrivia
Validation
Suppose we had a sendEmail function
sendEmail :: String — email address
-> String — message
-> IO () — action (more in 2 wks)
It is possible to mix the two String arguments, and even if we get the order right, it’s
possible that the given email address is not valid.
Question
Suppose that we wanted to make it impossible to call sendEmail without first
checking that the email address was valid.
How would we accomplish this?
11
Data Invariants and ADTs Validation Data Refinement Administrivia
Validation ADTs
We could define a tiny ADT for validated email addresses, where the data invariant is
that the contained email address is valid:
module EmailADT(Email, checkEmail, sendEmail)
newtype Email = Email String
checkEmail :: String -> Maybe Email
checkEmail str | ‘@’ `elem` str = Just (Email str)
| otherwise = Nothing
Then, change the type of sendEmail:
sendEmail :: Email -> String -> IO()
The only way (outside of the EmailADT module) to create a value of type Email is to
use checkEmail.
checkEmail is an example of what we call a smart constructor: a constructor that
enforces data invariants.
12
Data Invariants and ADTs Validation Data Refinement Administrivia
Validation ADTs
We could define a tiny ADT for validated email addresses, where the data invariant is
that the contained email address is valid:
module EmailADT(Email, checkEmail, sendEmail)
newtype Email = Email String
checkEmail :: String -> Maybe Email
checkEmail str | ‘@’ `elem` str = Just (Email str)
| otherwise = Nothing
Then, change the type of sendEmail:
sendEmail :: Email -> String -> IO()
The only way (outside of the EmailADT module) to create a value of type Email is to
use checkEmail.
checkEmail is an example of what we call a smart constructor: a constructor that
enforces data invariants.
13
Data Invariants and ADTs Validation Data Refinement Administrivia
Validation ADTs
We could define a tiny ADT for validated email addresses, where the data invariant is
that the contained email address is valid:
module EmailADT(Email, checkEmail, sendEmail)
newtype Email = Email String
checkEmail :: String -> Maybe Email
checkEmail str | ‘@’ `elem` str = Just (Email str)
| otherwise = Nothing
Then, change the type of sendEmail:
sendEmail :: Email -> String -> IO()
The only way (outside of the EmailADT module) to create a value of type Email is to
use checkEmail.
checkEmail is an example of what we call a smart constructor: a constructor that
enforces data invariants.
14
Data Invariants and ADTs Validation Data Refinement Administrivia
Validation ADTs
We could define a tiny ADT for validated email addresses, where the data invariant is
that the contained email address is valid:
module EmailADT(Email, checkEmail, sendEmail)
newtype Email = Email String
checkEmail :: String -> Maybe Email
checkEmail str | ‘@’ `elem` str = Just (Email str)
| otherwise = Nothing
Then, change the type of sendEmail:
sendEmail :: Email -> String -> IO()
The only way (outside of the EmailADT module) to create a value of type Email is to
use checkEmail.
checkEmail is an example of what we call a smart constructor: a constructor that
enforces data invariants.
15
Data Invariants and ADTs Validation Data Refinement Administrivia
Reasoning about ADTs
Consider the following, more traditional example of an ADT interface, the unbounded
queue:
data Queue
emptyQueue :: Queue
enqueue :: Int -> Queue -> Queue
front :: Queue -> Int — partial
dequeue :: Queue -> Queue — partial
size :: Queue -> Int
We could try to come up with properties that relate these functions to each other
without reference to their implementation, such as:
dequeue (enqueue x emptyQueue) == emptyQueue
However these do not capture functional correctness (usually).
16
Data Invariants and ADTs Validation Data Refinement Administrivia
Models for ADTs
We could imagine a simple implementation for queues, just in terms of lists:
emptyQueueL = []
enqueueL a = (++ [a])
frontL = head
dequeueL = tail
sizeL = length
But this implementation is O(n) to enqueue! Unacceptable!
However!
This is a dead simple implementation, and trivial to see that it is correct. If we make a
better queue implementation, it should always give the same results as this simple one.
Therefore: This implementation serves as a functional correctness specification for our
Queue type!
17
Data Invariants and ADTs Validation Data Refinement Administrivia
Models for ADTs
We could imagine a simple implementation for queues, just in terms of lists:
emptyQueueL = []
enqueueL a = (++ [a])
frontL = head
dequeueL = tail
sizeL = length
But this implementation is O(n) to enqueue! Unacceptable!
However!
This is a dead simple implementation, and trivial to see that it is correct. If we make a
better queue implementation, it should always give the same results as this simple one.
Therefore: This implementation serves as a functional correctness specification for our
Queue type!
18
Data Invariants and ADTs Validation Data Refinement Administrivia
Models for ADTs
We could imagine a simple implementation for queues, just in terms of lists:
emptyQueueL = []
enqueueL a = (++ [a])
frontL = head
dequeueL = tail
sizeL = length
But this implementation is O(n) to enqueue! Unacceptable!
However!
This is a dead simple implementation, and trivial to see that it is correct. If we make a
better queue implementation, it should always give the same results as this simple one.
Therefore: This implementation serves as a functional correctness specification for our
Queue type!
19
Data Invariants and ADTs Validation Data Refinement Administrivia
Models for ADTs
We could imagine a simple implementation for queues, just in terms of lists:
emptyQueueL = []
enqueueL a = (++ [a])
frontL = head
dequeueL = tail
sizeL = length
But this implementation is O(n) to enqueue! Unacceptable!
However!
This is a dead simple implementation, and trivial to see that it is correct. If we make a
better queue implementation, it should always give the same results as this simple one.
Therefore: This implementation serves as a functional correctness specification for our
Queue type!
20
Data Invariants and ADTs Validation Data Refinement Administrivia
Refinement Relations
The typical approach to connect our model queue to our Queue type is to define a
relation, called a refinement relation, that relates a Queue to a list and tells us if the
two structures represent the same queue conceptually:
rel :: Queue -> [Int] -> Bool
Then, we show that the refinement relation holds initially:
prop_empty_r = rel emptyQueue emptyQueueL
That any query functions for our two types produce equal results for related inputs,
such as for size:
prop_size_r fq lq = rel fq lq ==> size fq == sizeL lq
And that each of the queue operations preserves our refinement relation, for example
for enqueue:
prop_enq_ref fq lq x =
rel fq lq ==> rel (enqueue x fq) (enqueueL x lq)
21
Data Invariants and ADTs Validation Data Refinement Administrivia
Refinement Relations
The typical approach to connect our model queue to our Queue type is to define a
relation, called a refinement relation, that relates a Queue to a list and tells us if the
two structures represent the same queue conceptually:
rel :: Queue -> [Int] -> Bool
Then, we show that the refinement relation holds initially:
prop_empty_r = rel emptyQueue emptyQueueL
That any query functions for our two types produce equal results for related inputs,
such as for size:
prop_size_r fq lq = rel fq lq ==> size fq == sizeL lq
And that each of the queue operations preserves our refinement relation, for example
for enqueue:
prop_enq_ref fq lq x =
rel fq lq ==> rel (enqueue x fq) (enqueueL x lq)
22
Data Invariants and ADTs Validation Data Refinement Administrivia
Refinement Relations
The typical approach to connect our model queue to our Queue type is to define a
relation, called a refinement relation, that relates a Queue to a list and tells us if the
two structures represent the same queue conceptually:
rel :: Queue -> [Int] -> Bool
Then, we show that the refinement relation holds initially:
prop_empty_r = rel emptyQueue emptyQueueL
That any query functions for our two types produce equal results for related inputs,
such as for size:
prop_size_r fq lq = rel fq lq ==> size fq == sizeL lq
And that each of the queue operations preserves our refinement relation, for example
for enqueue:
prop_enq_ref fq lq x =
rel fq lq ==> rel (enqueue x fq) (enqueueL x lq)
23
Data Invariants and ADTs Validation Data Refinement Administrivia
Refinement Relations
The typical approach to connect our model queue to our Queue type is to define a
relation, called a refinement relation, that relates a Queue to a list and tells us if the
two structures represent the same queue conceptually:
rel :: Queue -> [Int] -> Bool
Then, we show that the refinement relation holds initially:
prop_empty_r = rel emptyQueue emptyQueueL
That any query functions for our two types produce equal results for related inputs,
such as for size:
prop_size_r fq lq = rel fq lq ==> size fq == sizeL lq
And that each of the queue operations preserves our refinement relation, for example
for enqueue:
prop_enq_ref fq lq x =
rel fq lq ==> rel (enqueue x fq) (enqueueL x lq)
24
Data Invariants and ADTs Validation Data Refinement Administrivia
In Pictures
• • • • . . .
emptyQueue enqueue 2 enqueue 7 dequeue
[] [2] [2,7] · · ·
0
size
prop size r fq lq = rel fq lq ==> size fq == sizeL lq
25
Data Invariants and ADTs Validation Data Refinement Administrivia
In Pictures
• • • • . . .
emptyQueue enqueue 2 enqueue 7 dequeue
prop empty r = rel emptyQueue emptyQueueL
[]
[2] [2,7] · · ·
0
size
prop size r fq lq = rel fq lq ==> size fq == sizeL lq
26
Data Invariants and ADTs Validation Data Refinement Administrivia
In Pictures
• • • • . . .
emptyQueue enqueue 2 enqueue 7 dequeue
[]
prop enq ref fq lq x =
rel fq lq ==> ref (enqueue x fq) (enqueueL x lq)
[2]
[2,7] · · ·
0
size
prop size r fq lq = rel fq lq ==> size fq == sizeL lq
27
Data Invariants and ADTs Validation Data Refinement Administrivia
In Pictures
• • • • . . .
emptyQueue enqueue 2 enqueue 7 dequeue
[]
prop enq ref fq lq x =
rel fq lq ==> ref (enqueue x fq) (enqueueL x lq)
[2] [2,7]
· · ·
0
size
prop size r fq lq = rel fq lq ==> size fq == sizeL lq
28
Data Invariants and ADTs Validation Data Refinement Administrivia
In Pictures
• • • • . . .
emptyQueue enqueue 2 enqueue 7 dequeue
[] [2] [2,7] · · ·
0
size
prop size r fq lq = rel fq lq ==> size fq == sizeL lq
29
Data Invariants and ADTs Validation Data Refinement Administrivia
In Pictures
• • • • . . .
emptyQueue enqueue 2 enqueue 7 dequeue
[] [2] [2,7] · · ·
0
size
prop size r fq lq = rel fq lq ==> size fq == sizeL lq
30
Data Invariants and ADTs Validation Data Refinement Administrivia
In Pictures
• • • • . . .
emptyQueue enqueue 2 enqueue 7 dequeue
[] [2] [2,7] · · ·
0
size
prop size r fq lq = rel fq lq ==> size fq == sizeL lq
Whenever we use a Queue, we can reason as if it were a list!
31
Data Invariants and ADTs Validation Data Refinement Administrivia
In Pictures
• • • • . . .
emptyQueue enqueue 2 enqueue 7 dequeue
[] [2] [2,7] · · ·
0
size
prop size r fq lq = rel fq lq ==> size fq == sizeL lq
Whenever we use a Queue, we can reason as if it were a list!
32
Data Invariants and ADTs Validation Data Refinement Administrivia
Abstraction Functions
These refinement relations are very difficult to use with QuickCheck because the rel
fq lq preconditions are very hard to satisfy with randomly generated inputs.
For this example, it’s a lot easier if we define an abstraction function that computes
the corresponding abstract list from the concrete Queue.
toAbstract :: Queue→ [Int]
Conceptually, our refinement relation is then just:
\fq lq→ absfun fq == lq
However, we can re-express our properties in a much more QC-friendly format (Demo)
33
Data Invariants and ADTs Validation Data Refinement Administrivia
Abstraction Functions
These refinement relations are very difficult to use with QuickCheck because the rel
fq lq preconditions are very hard to satisfy with randomly generated inputs.
For this example, it’s a lot easier if we define an abstraction function that computes
the corresponding abstract list from the concrete Queue.
toAbstract :: Queue→ [Int]
Conceptually, our refinement relation is then just:
\fq lq→ absfun fq == lq
However, we can re-express our properties in a much more QC-friendly format (Demo)
34
Data Invariants and ADTs Validation Data Refinement Administrivia
Abstraction Functions
These refinement relations are very difficult to use with QuickCheck because the rel
fq lq preconditions are very hard to satisfy with randomly generated inputs.
For this example, it’s a lot easier if we define an abstraction function that computes
the corresponding abstract list from the concrete Queue.
toAbstract :: Queue→ [Int]
Conceptually, our refinement relation is then just:
\fq lq→ absfun fq == lq
However, we can re-express our properties in a much more QC-friendly format (Demo)
35
Data Invariants and ADTs Validation Data Refinement Administrivia
Fast Queues
Let’s use test-driven development! We’ll implement a fast Queue with amortised O(1)
operations.
data Queue = Q [Int] — front of the queue
Int — size of the front
[Int] — rear of the queue
Int — size of the rear
We store the rear part of the queue in reverse order, to make enqueueing easier.
Thus, converting from our Queue to an abstract list requires us to reverse the rear:
toAbstract :: Queue -> [Int]
toAbstract (Q f sf r sr) = f ++ reverse r
36
Data Invariants and ADTs Validation Data Refinement Administrivia
Fast Queues
Let’s use test-driven development! We’ll implement a fast Queue with amortised O(1)
operations.
data Queue = Q [Int] — front of the queue
Int — size of the front
[Int] — rear of the queue
Int — size of the rear
We store the rear part of the queue in reverse order, to make enqueueing easier.
Thus, converting from our Queue to an abstract list requires us to reverse the rear:
toAbstract :: Queue -> [Int]
toAbstract (Q f sf r sr) = f ++ reverse r
37
Data Invariants and ADTs Validation Data Refinement Administrivia
Data Refinement
These kinds of properties establish what is known as a data refinement from the
abstract, slow, list model to the fast, concrete Queue implementation.
Refinement and Specifications
In general, all functional correctness specifications can be expressed as:
1 all data invariants are maintained, and
2 the implementation is a refinement of an abstract correctness model.
There is a limit to the amount of abstraction we can do before they become useless for
testing (but not necessarily for proving).
Warning
While abstraction can simplify proofs, abstraction does not reduce the fundamental
complexity of verification, which is provably hard.
38
Data Invariants and ADTs Validation Data Refinement Administrivia
Data Refinement
These kinds of properties establish what is known as a data refinement from the
abstract, slow, list model to the fast, concrete Queue implementation.
Refinement and Specifications
In general, all functional correctness specifications can be expressed as:
1 all data invariants are maintained, and
2 the implementation is a refinement of an abstract correctness model.
There is a limit to the amount of abstraction we can do before they become useless for
testing (but not necessarily for proving).
Warning
While abstraction can simplify proofs, abstraction does not reduce the fundamental
complexity of verification, which is provably hard.
39
Data Invariants and ADTs Validation Data Refinement Administrivia
Data Refinement
These kinds of properties establish what is known as a data refinement from the
abstract, slow, list model to the fast, concrete Queue implementation.
Refinement and Specifications
In general, all functional correctness specifications can be expressed as:
1 all data invariants are maintained, and
2 the implementation is a refinement of an abstract correctness model.
There is a limit to the amount of abstraction we can do before they become useless for
testing (but not necessarily for proving).
Warning
While abstraction can simplify proofs, abstraction does not reduce the fundamental
complexity of verification, which is provably hard.
40
Data Invariants and ADTs Validation Data Refinement Administrivia
Data Refinement
These kinds of properties establish what is known as a data refinement from the
abstract, slow, list model to the fast, concrete Queue implementation.
Refinement and Specifications
In general, all functional correctness specifications can be expressed as:
1 all data invariants are maintained, and
2 the implementation is a refinement of an abstract correctness model.
There is a limit to the amount of abstraction we can do before they become useless for
testing (but not necessarily for proving).
Warning
While abstraction can simplify proofs, abstraction does not reduce the fundamental
complexity of verification, which is provably hard.
41
Data Invariants and ADTs Validation Data Refinement Administrivia
Data Refinement
These kinds of properties establish what is known as a data refinement from the
abstract, slow, list model to the fast, concrete Queue implementation.
Refinement and Specifications
In general, all functional correctness specifications can be expressed as:
1 all data invariants are maintained, and
2 the implementation is a refinement of an abstract correctness model.
There is a limit to the amount of abstraction we can do before they become useless for
testing (but not necessarily for proving).
Warning
While abstraction can simplify proofs, abstraction does not reduce the fundamental
complexity of verification, which is provably hard.
42
Data Invariants and ADTs Validation Data Refinement Administrivia
Data Invariants for Queue
In addition to the already-stated refinement properties, we also have some data
invariants to maintain for a value Q f sf r sr:
1 length f == sf
2 length r == sr
3 important: sf ≥ sr — the front of the queue cannot be shorter than the rear.
We will ensure our Arbitrary instance only ever generates values that meet these
invariants.
Thus, our wellformed predicate is used merely to enforce these data invariants on the
outputs of our operations:
prop_wf_empty = wellformed (emptyQueue)
prop_wf_enq q = wellformed (enqueue x q)
prop_wf_deq q = size q > 0 ==> wellformed (dequeue q)
43
Data Invariants and ADTs Validation Data Refinement Administrivia
Data Invariants for Queue
In addition to the already-stated refinement properties, we also have some data
invariants to maintain for a value Q f sf r sr:
1 length f == sf
2 length r == sr
3 important: sf ≥ sr — the front of the queue cannot be shorter than the rear.
We will ensure our Arbitrary instance only ever generates values that meet these
invariants.
Thus, our wellformed predicate is used merely to enforce these data invariants on the
outputs of our operations:
prop_wf_empty = wellformed (emptyQueue)
prop_wf_enq q = wellformed (enqueue x q)
prop_wf_deq q = size q > 0 ==> wellformed (dequeue q)
44
Data Invariants and ADTs Validation Data Refinement Administrivia
Data Invariants for Queue
In addition to the already-stated refinement properties, we also have some data
invariants to maintain for a value Q f sf r sr:
1 length f == sf
2 length r == sr
3 important: sf ≥ sr — the front of the queue cannot be shorter than the rear.
We will ensure our Arbitrary instance only ever generates values that meet these
invariants.
Thus, our wellformed predicate is used merely to enforce these data invariants on the
outputs of our operations:
prop_wf_empty = wellformed (emptyQueue)
prop_wf_enq q = wellformed (enqueue x q)
prop_wf_deq q = size q > 0 ==> wellformed (dequeue q)
45
Data Invariants and ADTs Validation Data Refinement Administrivia
Data Invariants for Queue
In addition to the already-stated refinement properties, we also have some data
invariants to maintain for a value Q f sf r sr:
1 length f == sf
2 length r == sr
3 important: sf ≥ sr — the front of the queue cannot be shorter than the rear.
We will ensure our Arbitrary instance only ever generates values that meet these
invariants.
Thus, our wellformed predicate is used merely to enforce these data invariants on the
outputs of our operations:
prop_wf_empty = wellformed (emptyQueue)
prop_wf_enq q = wellformed (enqueue x q)
prop_wf_deq q = size q > 0 ==> wellformed (dequeue q)
46
Data Invariants and ADTs Validation Data Refinement Administrivia
Data Invariants for Queue
In addition to the already-stated refinement properties, we also have some data
invariants to maintain for a value Q f sf r sr:
1 length f == sf
2 length r == sr
3 important: sf ≥ sr — the front of the queue cannot be shorter than the rear.
We will ensure our Arbitrary instance only ever generates values that meet these
invariants.
Thus, our wellformed predicate is used merely to enforce these data invariants on the
outputs of our operations:
prop_wf_empty = wellformed (emptyQueue)
prop_wf_enq q = wellformed (enqueue x q)
prop_wf_deq q = size q > 0 ==> wellformed (dequeue q)
47
Data Invariants and ADTs Validation Data Refinement Administrivia
Implementing the Queue
We will generally implement by:
Dequeue from the front.
Enqueue to the rear.
If necessary, re-establish the third data invariant by taking the rear, reversing it,
and appending it to the front.
This step is slow (O(n)), but only happens every n operations or so, giving an
average case amortised complexity of O(1) time.
48
Data Invariants and ADTs Validation Data Refinement Administrivia
Implementing the Queue
We will generally implement by:
Dequeue from the front.
Enqueue to the rear.
If necessary, re-establish the third data invariant by taking the rear, reversing it,
and appending it to the front.
This step is slow (O(n)), but only happens every n operations or so, giving an
average case amortised complexity of O(1) time.
49
Data Invariants and ADTs Validation Data Refinement Administrivia
Amortised Cost
enqueue x (Q f sf r sr) = inv3 (Q f sf (x:r) (sr + 1))
When we enqueue each of [1..7] to the emptyQueue in turn:
Q [] 0 [] 0
→ Q [1] 1 [] 0 (∗)
→ Q [1] 1 [2] 1
→ Q [1, 2, 3] 3 [] 0 (∗)
→ Q [1, 2, 3] 3 [4] 1
→ Q [1, 2, 3] 3 [5, 4] 2
→ Q [1, 2, 3] 3 [6, 5, 4] 3
→ Q [1, 2, 3, 4, 5, 6, 7] 7 [] 0 (∗)
Observe that the slow invariant-reestablishing step (∗) happens after 1 step, then 2,
then 4. . .
Extended out, this averages out to O(1).
50
Data Invariants and ADTs Validation Data Refinement Administrivia
Amortised Cost
enqueue x (Q f sf r sr) = inv3 (Q f sf (x:r) (sr + 1))
When we enqueue each of [1..7] to the emptyQueue in turn:
Q [] 0 [] 0
→ Q [1] 1 [] 0 (∗)
→ Q [1] 1 [2] 1
→ Q [1, 2, 3] 3 [] 0 (∗)
→ Q [1, 2, 3] 3 [4] 1
→ Q [1, 2, 3] 3 [5, 4] 2
→ Q [1, 2, 3] 3 [6, 5, 4] 3
→ Q [1, 2, 3, 4, 5, 6, 7] 7 [] 0 (∗)
Observe that the slow invariant-reestablishing step (∗) happens after 1 step, then 2,
then 4. . .
Extended out, this averages out to O(1).
51
Data Invariants and ADTs Validation Data Refinement Administrivia
Amortised Cost
enqueue x (Q f sf r sr) = inv3 (Q f sf (x:r) (sr + 1))
When we enqueue each of [1..7] to the emptyQueue in turn:
Q [] 0 [] 0
→ Q [1] 1 [] 0 (∗)
→ Q [1] 1 [2] 1
→ Q [1, 2, 3] 3 [] 0 (∗)
→ Q [1, 2, 3] 3 [4] 1
→ Q [1, 2, 3] 3 [5, 4] 2
→ Q [1, 2, 3] 3 [6, 5, 4] 3
→ Q [1, 2, 3, 4, 5, 6, 7] 7 [] 0 (∗)
Observe that the slow invariant-reestablishing step (∗) happens after 1 step, then 2,
then 4. . .
Extended out, this averages out to O(1).
52
Data Invariants and ADTs Validation Data Refinement Administrivia
Amortised Cost
enqueue x (Q f sf r sr) = inv3 (Q f sf (x:r) (sr + 1))
When we enqueue each of [1..7] to the emptyQueue in turn:
Q [] 0 [] 0
→ Q [1] 1 [] 0 (∗)
→ Q [1] 1 [2] 1
→ Q [1, 2, 3] 3 [] 0 (∗)
→ Q [1, 2, 3] 3 [4] 1
→ Q [1, 2, 3] 3 [5, 4] 2
→ Q [1, 2, 3] 3 [6, 5, 4] 3
→ Q [1, 2, 3, 4, 5, 6, 7] 7 [] 0 (∗)
Observe that the slow invariant-reestablishing step (∗) happens after 1 step, then 2,
then 4. . .
Extended out, this averages out to O(1).
53
Data Invariants and ADTs Validation Data Refinement Administrivia
Amortised Cost
enqueue x (Q f sf r sr) = inv3 (Q f sf (x:r) (sr + 1))
When we enqueue each of [1..7] to the emptyQueue in turn:
Q [] 0 [] 0
→ Q [1] 1 [] 0 (∗)
→ Q [1] 1 [2] 1
→ Q [1, 2, 3] 3 [] 0 (∗)
→ Q [1, 2, 3] 3 [4] 1
→ Q [1, 2, 3] 3 [5, 4] 2
→ Q [1, 2, 3] 3 [6, 5, 4] 3
→ Q [1, 2, 3, 4, 5, 6, 7] 7 [] 0 (∗)
Observe that the slow invariant-reestablishing step (∗) happens after 1 step, then 2,
then 4. . .
Extended out, this averages out to O(1).
54
Data Invariants and ADTs Validation Data Refinement Administrivia
Amortised Cost
enqueue x (Q f sf r sr) = inv3 (Q f sf (x:r) (sr + 1))
When we enqueue each of [1..7] to the emptyQueue in turn:
Q [] 0 [] 0
→ Q [1] 1 [] 0 (∗)
→ Q [1] 1 [2] 1
→ Q [1, 2, 3] 3 [] 0 (∗)
→ Q [1, 2, 3] 3 [4] 1
→ Q [1, 2, 3] 3 [5, 4] 2
→ Q [1, 2, 3] 3 [6, 5, 4] 3
→ Q [1, 2, 3, 4, 5, 6, 7] 7 [] 0 (∗)
Observe that the slow invariant-reestablishing step (∗) happens after 1 step, then 2,
then 4. . .
Extended out, this averages out to O(1).
55
Data Invariants and ADTs Validation Data Refinement Administrivia
Amortised Cost
enqueue x (Q f sf r sr) = inv3 (Q f sf (x:r) (sr + 1))
When we enqueue each of [1..7] to the emptyQueue in turn:
Q [] 0 [] 0
→ Q [1] 1 [] 0 (∗)
→ Q [1] 1 [2] 1
→ Q [1, 2, 3] 3 [] 0 (∗)
→ Q [1, 2, 3] 3 [4] 1
→ Q [1, 2, 3] 3 [5, 4] 2
→ Q [1, 2, 3] 3 [6, 5, 4] 3
→ Q [1, 2, 3, 4, 5, 6, 7] 7 [] 0 (∗)
Observe that the slow invariant-reestablishing step (∗) happens after 1 step, then 2,
then 4. . .
Extended out, this averages out to O(1).
56
Data Invariants and ADTs Validation Data Refinement Administrivia
Amortised Cost
enqueue x (Q f sf r sr) = inv3 (Q f sf (x:r) (sr + 1))
When we enqueue each of [1..7] to the emptyQueue in turn:
Q [] 0 [] 0
→ Q [1] 1 [] 0 (∗)
→ Q [1] 1 [2] 1
→ Q [1, 2, 3] 3 [] 0 (∗)
→ Q [1, 2, 3] 3 [4] 1
→ Q [1, 2, 3] 3 [5, 4] 2
→ Q [1, 2, 3] 3 [6, 5, 4] 3
→ Q [1, 2, 3, 4, 5, 6, 7] 7 [] 0 (∗)
Observe that the slow invariant-reestablishing step (∗) happens after 1 step, then 2,
then 4. . .
Extended out, this averages out to O(1).
57
Data Invariants and ADTs Validation Data Refinement Administrivia
Amortised Cost
enqueue x (Q f sf r sr) = inv3 (Q f sf (x:r) (sr + 1))
When we enqueue each of [1..7] to the emptyQueue in turn:
Q [] 0 [] 0
→ Q [1] 1 [] 0 (∗)
→ Q [1] 1 [2] 1
→ Q [1, 2, 3] 3 [] 0 (∗)
→ Q [1, 2, 3] 3 [4] 1
→ Q [1, 2, 3] 3 [5, 4] 2
→ Q [1, 2, 3] 3 [6, 5, 4] 3
→ Q [1, 2, 3, 4, 5, 6, 7] 7 [] 0 (∗)
Observe that the slow invariant-reestablishing step (∗) happens after 1 step, then 2,
then 4. . .
Extended out, this averages out to O(1).
58
Data Invariants and ADTs Validation Data Refinement Administrivia
Another Example
Consider this ADT interface for a bag of numbers:
data Bag
emptyBag :: Bag
addToBag :: Int -> Bag -> Bag
averageBag :: Bag -> Maybe Int
Our conceptual abstract model is just a list of numbers:
emptyBagA = []
addToBagA x xs = x:xs
averageBagA [] = Nothing
averageBagA xs = Just (sum xs `div` length xs)
But do we need to keep track of all that information in our implementation? No!
59
Data Invariants and ADTs Validation Data Refinement Administrivia
Another Example
Consider this ADT interface for a bag of numbers:
data Bag
emptyBag :: Bag
addToBag :: Int -> Bag -> Bag
averageBag :: Bag -> Maybe Int
Our conceptual abstract model is just a list of numbers:
emptyBagA = []
addToBagA x xs = x:xs
averageBagA [] = Nothing
averageBagA xs = Just (sum xs `div` length xs)
But do we need to keep track of all that information in our implementation?
No!
60
Data Invariants and ADTs Validation Data Refinement Administrivia
Another Example
Consider this ADT interface for a bag of numbers:
data Bag
emptyBag :: Bag
addToBag :: Int -> Bag -> Bag
averageBag :: Bag -> Maybe Int
Our conceptual abstract model is just a list of numbers:
emptyBagA = []
addToBagA x xs = x:xs
averageBagA [] = Nothing
averageBagA xs = Just (sum xs `div` length xs)
But do we need to keep track of all that information in our implementation? No!
61
Data Invariants and ADTs Validation Data Refinement Administrivia
Concrete Implementation
Our concrete version will just maintain two integers, the total and the count:
data Bag = B { total :: Int , count :: Int }
emptyBag :: Bag
emptyBag = B 0 0
addToBag :: Int -> Bag -> Bag
addToBag x (B t c) = B (x + t) (c + 1)
averageBag :: Bag -> Maybe Int
averageBag (B _ 0) = Nothing
averageBag (B t c) = Just (t `div` c)
62
Data Invariants and ADTs Validation Data Refinement Administrivia
Refinement Functions
Normally, writing an abstraction function (as we did for Queue) is a good way to
express our refinement relation in a QC-friendly way. In this case, however, it’s hard to
write such a function:
toAbstract :: Bag -> [Int]
toAbstract (B t c) = ?????
Instead, we will go in the other direction, giving us a refinement function:
toConc :: [Int] -> Bag
toConc xs = B (sum xs) (length xs)
63
Data Invariants and ADTs Validation Data Refinement Administrivia
Properties with Refinement Functions
Refinement functions produce properties much like abstraction functions, only with the
abstract and concrete layers swapped:
prop_ref_empty =
toConc emptyBagA == emptyBag
prop_ref_add x ab =
toConc (addToBagA x ab) == addToBag x (toConc ab)
prop_ref_avg ab =
averageBagA ab == averageBag (toConc ab)
64
Data Invariants and ADTs Validation Data Refinement Administrivia
Assignment 1 and Break
Assignment 1 has been released.
It is due right before the Friday Lecture of Week 5.
Advice from Alumni
The assignments do not involve much coding, but they do involve a lot of thinking.
Start early!
65
Data Invariants and ADTs Validation Data Refinement Administrivia
Assignment 1 and Break
Assignment 1 has been released.
It is due right before the Friday Lecture of Week 5.
Advice from Alumni
The assignments do not involve much coding, but they do involve a lot of thinking.
Start early!
66
Data Invariants and ADTs Validation Data Refinement Administrivia
Assignment 1 and Break
Assignment 1 has been released.
It is due right before the Friday Lecture of Week 5.
Advice from Alumni
The assignments do not involve much coding, but they do involve a lot of thinking.
Start early!
67
Data Invariants and ADTs Validation Data Refinement Administrivia
Homework
1 Get started on Assignment 1.
2 Next programming exercise is out, due before Friday 12pm.
3 Last week’s quiz is due this Friday 6pm. Make sure you submit your answers.
4 This week’s quiz is also up, due the following Friday.
68
Data Invariants and ADTs
Validation
Data Refinement
Administrivia