Documentation.SBV.Examples.BitPrecise.MergeSort

Symbolic implementation of merge-sort and its correctness.

Implementing Merge-Sort

type E = SWord8

Element type of lists we'd like to sort. For simplicity, we'll just use SWord8 here, but we can pick any symbolic type.

merge :: [E] -> [E] -> [E]

Merging two given sorted lists, preserving the order.

mergeSort :: [E] -> [E]

Simple merge-sort implementation. We simply divide the input list in two halves so long as it has at least two elements, sort each half on its own, and then merge.

Proving correctness

There are two main parts to proving that a sorting algorithm is correct:

• Prove that the output is non-decreasing
• Prove that the output is a permutation of the input

nonDecreasing :: [E] -> SBool

Check whether a given sequence is non-decreasing.

isPermutationOf :: [E] -> [E] -> SBool

Check whether two given sequences are permutations. We simply check that each sequence is a subset of the other, when considered as a set. The check is slightly complicated for the need to account for possibly duplicated elements.

correctness :: Int -> IO ThmResult

Asserting correctness of merge-sort for a list of the given size. Note that we can only check correctness for fixed-size lists. Also, the proof will get more and more complicated for the backend SMT solver as the list size increases. A value around 5 or 6 should be fairly easy to prove. For instance, we have:

>>> correctness 5
Q.E.D.

Generating C code

codeGen :: Int -> IO ()

Generate C code for merge-sorting an array of size n. Again, we're restricted to fixed size inputs. While the output is not how one would code merge sort in C by hand, it's a faithful rendering of all the operations merge-sort would do as described by its Haskell counterpart.