CS计算机代考程序代写 Haskell COMP3141 – Data Invariants, Abstraction and Refinement

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