程序代写代做代考 C go Haskell Data Invariants and ADTs Validation Data Refinement Administrivia

Data Invariants and ADTs Validation Data Refinement Administrivia
1
Software System Design and Implementation
Data Invariants, Abstraction and Refinement
Liam O’Connor
University of Edinburgh LFCS (and UNSW) Term 2 2020

Data Invariants and ADTs Validation Data Refinement Administrivia
2
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?

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:
• to query information from the data type:
• to update the data type:
A lot of software can be designed with this structure.
Example (Data Types)
A dictionary data type, with empty, insert and lookup.
c :: ··· → X q :: X → · · · u :: ···X → X
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
7
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.

Data Invariants and ADTs Validation Data Refinement Administrivia
8
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.

Data Invariants and ADTs Validation Data Refinement Administrivia
9
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.

Data Invariants and ADTs Validation Data Refinement Administrivia
10
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.

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
12
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

Data Invariants and ADTs Validation Data Refinement Administrivia
13
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()

Data Invariants and ADTs Validation Data Refinement Administrivia
14
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.

Data Invariants and ADTs Validation Data Refinement Administrivia
15
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.

Data Invariants and ADTs Validation Data Refinement Administrivia
16
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).

Data Invariants and ADTs Validation Data Refinement Administrivia
17
Models for ADTs
We could imagine a simple implementation for queues, just in terms of lists:

Data Invariants and ADTs Validation Data Refinement Administrivia
18
Models for ADTs
We could imagine a simple implementation for queues, just in terms of lists:
emptyQueueL = []
enqueueL a = (++ [a])
frontL
dequeueL
sizeL
= head
= tail
= length

Data Invariants and ADTs Validation Data Refinement Administrivia
19
Models for ADTs
We could imagine a simple implementation for queues, just in terms of lists:
emptyQueueL = []
enqueueL a = (++ [a])
frontL
dequeueL
sizeL
= head
= tail
= length
But this implementation is O(n) to enqueue! Unacceptable!

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
dequeueL
sizeL
= head
= tail
= 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
21
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

Data Invariants and ADTs Validation Data Refinement Administrivia
22
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

Data Invariants and ADTs Validation Data Refinement Administrivia
23
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

Data Invariants and ADTs Validation Data Refinement Administrivia
24
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)

Data Invariants and ADTs Validation Data Refinement Administrivia
••••
…
In Pictures
emptyQueue enqueue 2 enqueue 7 dequeue

Data Invariants and ADTs
Validation
Data Refinement
Administrivia
[]
In Pictures
••••
emptyQueue enqueue 2 enqueue 7
…
prop empty r = rel emptyQueue emptyQueueL
dequeue

Data Invariants and ADTs Validation
Data Refinement
Administrivia
In Pictures
[] [2]
••••
emptyQueue enqueue 2 enqueue 7
…
propenqref fq lq x =
rel fq lq ==> ref (enqueue x fq) (enqueueL x lq)
dequeue

Data Invariants and ADTs Validation Data Refinement Administrivia
In Pictures
[] [2] [2,7]
••••
…
emptyQueue enqueue 2 enqueue 7 dequeue
propenqref fq lq x =
rel fq lq ==> ref (enqueue x fq) (enqueueL x lq)

Data Invariants and ADTs Validation Data Refinement Administrivia
In Pictures
[] [2] [2,7] ···
••••
…
emptyQueue enqueue 2 enqueue 7 dequeue

Data Invariants and ADTs Validation Data Refinement Administrivia
In Pictures
[] [2] [2,7] ···
••••
…
emptyQueue enqueue 2 size
enqueue 7 dequeue
0

Data Invariants and ADTs Validation Data Refinement Administrivia
In Pictures
[] [2] [2,7] ···
••••
…
emptyQueue enqueue 2 size
enqueue 7 dequeue
0
propsizer fq lq = rel fq lq ==> size fq == sizeL lq
31

Data Invariants and ADTs Validation Data Refinement Administrivia
33
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.

Data Invariants and ADTs Validation Data Refinement Administrivia
34
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]

Data Invariants and ADTs Validation Data Refinement Administrivia
35
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)

Data Invariants and ADTs Validation Data Refinement Administrivia
36
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.

Data Invariants and ADTs Validation Data Refinement Administrivia
37
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

Data Invariants and ADTs Validation Data Refinement Administrivia
38
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.

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).
41

Data Invariants and ADTs Validation Data Refinement Administrivia
43
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

Data Invariants and ADTs Validation Data Refinement Administrivia
44
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

Data Invariants and ADTs Validation Data Refinement Administrivia
45
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.

Data Invariants and ADTs Validation Data Refinement Administrivia
46
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.

Data Invariants and ADTs Validation Data Refinement Administrivia
47
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)

Data Invariants and ADTs Validation Data Refinement Administrivia
48
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.

Data Invariants and ADTs Validation Data Refinement Administrivia
49
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.

Data Invariants and ADTs Validation Data Refinement Administrivia
50
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

Data Invariants and ADTs Validation Data Refinement Administrivia
51
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 (∗)

Data Invariants and ADTs Validation Data Refinement Administrivia
52
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

Data Invariants and ADTs Validation Data Refinement Administrivia
53
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]
→ Q [1]
→ Q [1,2,3]
1 [] 0 (∗) 1 [2] 1
3 [] 0 (∗)

Data Invariants and ADTs Validation Data Refinement Administrivia
54
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]
→ Q [1] 1[2]1
→ Q [1, 2, 3]
→ Q [1, 2, 3] 3[4]1
1[]0 (∗)
3[]0 (∗)

Data Invariants and ADTs Validation Data Refinement Administrivia
55
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[]
→ Q [1]
→ Q [1]
0[]0
1 [] 0 (∗) 1 [2] 1
3 [] 0 (∗) 3 [4] 1
3 [5,4] 2
→ Q
→ Q
→ Q
[1, 2, 3] [1, 2, 3] [1, 2, 3]

Data Invariants and ADTs Validation Data Refinement Administrivia
56
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[]
→ Q [1]
→ Q [1]
0[]0
1 [] 0 (∗) 1 [2] 1
3 [] 0 (∗) 3 [4] 1
3 [5,4] 2
3 [6, 5, 4] 3
→ Q
→ Q
→ Q
→ Q
[1, 2, 3] [1, 2, 3] [1, 2, 3] [1, 2, 3]

Data Invariants and ADTs Validation Data Refinement Administrivia
57
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[]
→ Q [1]
→ Q [1]
0[]0
1 [] 0 (∗) 1 [2] 1
3 [] 0 (∗) 3 [4] 1
3 [5,4] 2
3 [6, 5, 4] 3
7 [] 0 (∗)
→ Q
→ Q
→ Q
→ Q
→ Q [1,2,3,4,5,6,7]
[1, 2, 3] [1, 2, 3] [1, 2, 3] [1, 2, 3]

Data Invariants and ADTs Validation Data Refinement Administrivia
58
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[]
→ Q [1]
→ Q [1]
0[]0
1 [] 0 (∗) 1 [2] 1
3 [] 0 (∗) 3 [4] 1
3 [5,4] 2
3 [6, 5, 4] 3
7 [] 0 (∗)
→ Q
→ Q
→ Q
→ Q
→ Q [1,2,3,4,5,6,7]
[1, 2, 3] [1, 2, 3] [1, 2, 3] [1, 2, 3]
Observe that the slow invariant-reestablishing step (∗) happens after 1 step, then 2, then 4. . .
Extended out, this averages out to O(1).

Data Invariants and ADTs Validation Data Refinement Administrivia
59
Another Example
Consider this ADT interface for a bag of numbers:
data Bag
emptyBag :: Bag
addToBag :: Int -> Bag -> Bag
averageBag :: Bag -> Maybe Int

Data Invariants and ADTs Validation Data Refinement Administrivia
60
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?

Data Invariants and ADTs Validation Data Refinement Administrivia
61
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!

Data Invariants and ADTs Validation Data Refinement Administrivia
62
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)

Data Invariants and ADTs Validation Data Refinement Administrivia
63
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)

Data Invariants and ADTs Validation Data Refinement Administrivia
64
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)

Data Invariants and ADTs Validation Data Refinement Administrivia
65
Assignment 1 has been released.
Assignment 1 and Break

Data Invariants and ADTs Validation Data Refinement Administrivia
66
Assignment 1 and Break
Assignment 1 has been released.
It is due right before the Wednesday Lecture of Week 5.

Data Invariants and ADTs Validation Data Refinement Administrivia
Assignment 1 and Break
Assignment 1 has been released.
It is due right before the Wednesday 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
68
Homework
1 Get started on Assignment 1.
2 Next programming exercise is out, due before 3pm Wed Week 5.
3 Last week’s quiz is due this Friday. Make sure you submit your answers.
4 This week’s quiz is also up, due the following Friday.

Related Posts