Exercise 2 Specification and Refinement Editor Example Administrivia
1
Software System Design and Implementation
Data Invariants, Abstraction and Refinement Practice
Curtis Millar
CSE, UNSW (and Data61) 24 June 2020
Exercise 2
Specification and Refinement
Editor Example
Administrivia
2
1
2 3 4 5
sortFn xs == sortFn (reverse xs)
x ¡®elem¡® sortFn (xs ++ [x] ++ ys)
isSorted (sortFn xs)
length xs == length (sortFn xs)
sortFn xs == insertionSort xs
Sort Properties
Exercise 2
Specification and Refinement
Editor Example
Administrivia
3
1
2 3 4
Satisfy only (2) and (4)
Satisfy only (1), (2), and (3) Satisfy only (1), (3), and (4) Satisfy only (1), (2), (3), and (4)
Dodgy Sort
Exercise 2
Specification and Refinement Editor Example Administrivia
4
Let¡¯s take a look at the gallery Assess your peers
Fractal Art
1 Is the function which generates the image a recursive function?
2 Is the picture function given parameters that influence at least two aspects of the
image other than recursion depth, size, and colour?
3 Is it a real attempt to generate a nice image?
Online form to review peers art & implementation on course website soon.
Exercise 2
Specification and Refinement Editor Example Administrivia
5
Data Invariants
Data invariants are statements that must always be true of a data structure. We generally represent these invariants as a wellformedness predicate, a function that tests whether a value is well-formed.
Data invaraints must be shown to be true for all constructors of a data type. The output of any constructor must satisfy the wellformedness predicate.
constructor :: .. -> X
Data invaraints must also be shown to be true for all functions that transform the value of a data type. The output of these functions must satisfy the wellformedness predicate only if the input does.
fn:: .. ->X->X
Exercise 2
Specification and Refinement Editor Example Administrivia
6
Abstract Data Types
ADTs allow us to encapsulate the implementation of a data type by restricting access to which functions can be used construct, query, or transform a value from outside the module in which it is defined.
The ability to restrict access to certain implementation details is generally dependant on the language.
If all the externally visible functions maintain the data invariants then no external code can construct a value that ever violates them.
Exercise 2
Specification and Refinement Editor Example Administrivia
7
Refinement
A relation from an implementation to an abstract model or an abstract specification.
If an implementation refines a model or specification, it exhibits all of the same behavior but may have additional behaviour or detail.
A refinement is the opposite of an abstraction, which removes detail.
In this course, the model and implementaion will present an indistingushable interface with different implementation details.
Exercise 2
Specification and Refinement Editor Example Administrivia
8
Data Refinement
We can demonstrate a refinement relation between two data types if we can show that the interfaces are the same and they exhibit the same behavior. This is a data refinement.
We choose which data type will be the abstract model which is the definition or specification.
The other data type then becomes our implementation, i.e. the data type that we will actually use in the final system.
We must show that the implementation is a refinement of the model or specification.
Exercise 2 Specification and Refinement Editor Example Administrivia
Data Refinement
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.
9
Exercise 2 Specification and Refinement Editor Example Administrivia
10
Consider this ADT interface for a text editor:
data Editor
einit :: String -> Editor
stringOf :: Editor -> String
moveLeft :: Editor -> Editor
moveRight :: Editor -> Editor
insertChar :: Char -> Editor -> Editor
deleteChar :: Editor -> Editor
Editor Example
Exercise 2 Specification and Refinement Editor Example Administrivia
11
Data Invariant Properties
prop_einit_ok
prop_moveLeft_ok
prop_moveRight_ok
prop_moveInsert_ok x a = wellformed (insertCharA x a)
prop_moveDelete_ok a = wellformed (deleteCharA a)
s = wellformed (einitA s)
a = wellformed (moveLeftA a)
a = wellformed (moveRightA a)
Exercise 2 Specification and Refinement Editor Example Administrivia
12
Editor Example: Abstract Model
Our conceptual abstract model is a string and a cursor position:
einitA s = A s 0
stringOfA (A s _) = s
moveLeftA (A t c) = A t (max 0 (c-1))
moveRightA (A t c) = A t (min (length t) (c+1))
insertCharA x (A t c) = let (t1, t2) = splitAt c t
in A (t1 ++ [x] ++ t2) (c+1)
deleteCharA (A t c) = let (t1, t2) = splitAt c t
in A (t1 ++ drop 1 t2) c
But do we need to keep track of all that information in our implementation? No!
Exercise 2 Specification and Refinement Editor Example Administrivia
13
Concrete Implementation
Our concrete version will just maintain two strings, the left part (in reverse) and the right part of the cursor:
einit s = C [] s
stringOf (C ls rs) = reverse ls ++ rs
moveLeft (C (l:ls) rs) = C ls (l:rs)
moveLeft c = c
moveRight (C ls (r:rs)) = C (r:ls) rs
moveRight c = c
insertChar x (C ls rs) = C (x:ls) rs
deleteChar (C ls (_:rs)) = C ls rs
deleteChar c = c
Exercise 2 Specification and Refinement Editor Example Administrivia
14
Refinement Functions
Abstraction function to express our refinement relation in a QC-friendly way: such a function:
toAbstract :: Concrete -> Abstract
toAbstract (C ls rs) = A (reverse ls ++ rs) (length ls)
Exercise 2 Specification and Refinement Editor Example Administrivia
15
Properties with Abstraction Functions
prop_init_r s =
toAbstract (einit s) == einitA s
prop_stringOf_r c =
stringOf c == stringOfA (toAbstract c)
prop_moveLeft_r c =
toAbstract (moveLeft c) == moveLeftA (toAbstract c)
prop_moveRight_r c =
toAbstract (moveRight c) == moveRightA (toAbstract c)
prop_insChar_r x c =
toAbstract (insertChar x c)
== insertCharA x (toAbstract c)
prop_delChar_r c =
toAbstract (deleteChar c) == deleteCharA (toAbstract c)
Exercise 2
Specification and Refinement Editor Example Administrivia
16
1
2 3 4
Last week¡¯s quiz is due on Friday. Make sure you submit your answers.
The third programming exercise is due by the start if my next lecture (in 7 days). The first assignment is due by the start if my next lecture (in 7 days).
This week¡¯s quiz is also up, it¡¯s due next Friday (in 9 days).
Homework
Exercise 2
Specification and Refinement Editor Example Administrivia
17
Consultations
Poll on Piazza to register interest. Will not run if there are no votes. Tomorrow, 9am to 11am on Blackboard Collaborate.
Link on course website & Piazza.
Make sure to join the queue on Hopper. Be ready to share your screen with REPL (ghci or stack repl) and editor set up.