Your solutions for this assignment should terminate within 20 seconds. If they exceed the time limit, you will get partial credit. Please also note how long your solutions take to run as a comment if they do exceed the time limit.
From Wikipedia:
The Dutch national flag problem (DNF) is a computer science programming problem proposed by Edsger Dijkstra. The flag of the Netherlands consists of three colours: red, white and blue. Given balls of these three colours arranged randomly in a line (the actual number of balls does not matter), the task is to arrange them such that all balls of the same colour are together and their collective colour groups are in the correct order. – https://en.wikipedia.org/wiki/Dutch_national_flag_problem
The problem is interesting because there is a sorting algorithm whose time complexity is linear and whose auxiliary memory is constant. The following pseudocode is an algorithm simplified from the one Wikipedia gives:
procedure dutch_sort(A : array of value):
i := 0
j := 0
n := size of A - 1
while j <= n:
if A[j] == Red:
swap A[i] and A[j]
i := i + 1
j := j + 1
else if A[j] == Blue:
swap A[j] and A[n]
n := n - 1
else:
j := j + 1
A loop invariant is a property that relates variable(s) and that holds before and after each iteration of an algorithm. In this part, you will informally list loop invariants of this algorithm in a file named invariants.txt, under Part 1.
Some examples of loop invariants (not for this problem) are:
i >= 1i + j + k < 2 * n - 1A[i...j] = 0Write 4 invariants inequalities (using <, >, <=, or >=) relating the values of i, j, n, len A, and numerical constants. Note that your inequalities should not be redundant - that is, you if you had “x < 10” and “y < x”, you should not have “y < 10”.
Also write 3 invariants (continued from the first 4 invariants) relating the entries of A and the colors Red, White, and Blue.
Consider the following buggy algorithm:
procedure buggy_sort_1(A : array of value):
i := 0
j := 0
n := size of A - 1
while j <= n:
if A[j] == Red:
swap A[i] and A[j]
i := i + 2 # <========== wrong
j := j + 1
else if A[j] == Blue:
swap A[j] and A[n]
n := n - 1
else:
j := j + 1
Then, buggy_sort_1([Red, Red]) will result in:
iteration 1: i = 0, j = 0, n = 1, A = [Red, Red]
iteration 2: i = 2, j = 1, n = 1, A = [Red, Red]
===> crash at "swap A[i] and A[j]" because the index is out of bound
Informally list which invariants (from Part 1) that this algorithm violates in the file invariants.txt, under Part 2.
So maybe it seems that if we have an algorithm which doesn’t violate any invariants, then it should be correct (in that it produces the expected output, without errors). Is this actually the case?
Consider another buggy algorithm:
procedure buggy_sort_2(A : array of value):
i := 0
j := 0
n := size of A - 1
while j <= n:
do nothing
Then, buggy_sort_2([Red, Blue]) will result in:
iteration 1: i = 0, j = 0, n = 1, A = [Red, Blue]
iteration 2: i = 0, j = 0, n = 1, A = [Red, Blue]
iteration 3: i = 0, j = 0, n = 1, A = [Red, Blue]
iteration 4: i = 0, j = 0, n = 1, A = [Red, Blue]
... (an infinite loop)
This algorithm doesn’t violate any invariants, but it doesn’t terminate!
How can we prove that an algorithm terminates? One way is to come up with a function which consumes variables in each iteration and produces a natural number (greater than or equal to zero). If we can show that this function is stricly decreasing as the algorithm progresses, we can guarantee that the function doesn’t continue forever! (And if the algorithm doesn’t terminate, it would be impossible to come up with such a function.)
For example, the quicksort algorithm could have the function T(L) = length of L, where L is the list to be sorted as a witness that the algorithm terminates. This is because T(L) >= 0 for all L, and in quicksort(L), the algorithm recursively calls itself with smaller lists, so T is decreasing.
Informally write down a stricly decreasing function T(A, i, j, n) = ... for dutch_sort in invariants.txt, under Part 3.
Your task is to write LH refinements to the stencil file such that correct implementations are
considered SAFE by LH, and crashing (index out of bound) or non-terminating programs are considered UNSAFE.
To simplify things, your refinement doesn’t need to invalidate incorrect programs which terminate and don’t crash.
We suggest that you to use LiquidHaskell via this browser-based IDE.
Although Haskell does have arrays and supports mutation in some contexts, due to the nature of functional programming, they tend to be difficult to use together. Therefore, we will convert the algorithm to a recurive (rather than iterative) style, using a (singly linked) list instead of an array and producing a new value instead of mutating variables. This makes the implementation very inefficient. However, since our goal here is to verify the correctness of the algorithm, this is fine. That is, although Haskell is a programming language in its own right, for the purpose of this problem we will treat it as a modeling language instead.
Note that LH has already added refinements to several functions in standard libraries, including an operator !!, used for getting the i-th element from a list. The refinement is to prevent the index to be out of bound. Thus, LH will consider the following UNSAFE:
foo :: Int -> Int
foo i = [1, 2, 3] !! i
unless you assure LH that i will not be out of bound.
Below is the stencil file, which has an implementation of the algorithm in functional style. Your task is to write refinements for loop and swap by filling in ..... Recall that .... in / [....] should be a decreasing expression (see Part 3).
{- Termination Check for Dutch national flag problem
(https://en.wikipedia.org/wiki/Dutch_national_flag_problem) -}
import Debug.Trace
data Color = Red | White | Blue deriving (Eq, Show, Ord)
dutchSort :: [Color] -> [Color]
dutchSort arr = loop arr 0 0 ((length arr) - 1)
-- note: add an opening @ here to un-comment this refinement
{- loop :: .... ->
.... ->
.... ->
.... ->
.... / [....] @-}
loop :: [Color] -> Int -> Int -> Int -> [Color]
loop arr i j n =
-- the next two lines are to print values in each iteration in ghci
trace
((show arr) ++ " " ++ (show i) ++ " " ++ (show j) ++ " " ++ (show n))
(if j <= n then
if arr!!j == Red then
loop (swap arr j i) (i + 1) (j + 1) n
else if arr!!j == Blue then
loop (swap arr j n) i j (n - 1)
else
loop arr i (j + 1) n
else
arr)
-- note: add an opening @ here to un-comment this refinement
{- swap :: .... ->
.... ->
.... ->
.... @-}
swap :: [Color] -> Int -> Int -> [Color]
swap arr i j = u2
where
u1 = update arr i (arr!!j)
u2 = update u1 j (arr!!i)
update arr i v = (take i arr) ++ [v] ++ (drop (i + 1) arr)
You can find a guide that covers the basic of Haskell on our notes page here. Another nice resource is tryhaskell.org, which provides a tutorial embedded into an interactive interpreter.
You can try running dutchSort (without the LiquidHaskell checks) on a department machine via Haskell’s REPL (ghci). Note that ghci must be executed in a directory that contains dutch.hs. You can modify the implementation so that it’s buggy and see how buggy dutchSort works too (but please make sure that when you submit it, the implementation is correct!)
$ ghci # run the REPL in the command line
GHCi, version 7.6.3: http://www.haskell.org/ghc/ :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> :l dutch -- load dutch.hs
[1 of 1] Compiling Main ( dutch.hs, interpreted )
Ok, modules loaded: Main.
*Main> dutchSort [Red, Blue, Red, White] -- call function dutchSort
[Red,Blue,Red,White] 0 0 3
[Red,Blue,Red,White] 1 1 3
[Red,White,Red,Blue] 1 1 2
[Red,White,Red,Blue] 1 2 2
[Red,Red,White,Blue] 2 3 2
[Red,Red,White,Blue]
*Main>
To exit ghci, press ctrl-d
Run cs195y_handin liquid from a directory holding dutch.hs and invariants.txt.
You should receive an email confirming that your handin has worked.