sbv-5.6: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Data.SBV.Examples.BitPrecise.MergeSort

Description

Symbolic implementation of merge-sort and its correctness.

Synopsis

# Implementing Merge-Sort

type E = SWord8 Source

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] Source

Merging two given sorted lists, preserving the order.

mergeSort :: [E] -> [E] Source

Simple merge-sort implementation. We simply divide the input list in two 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 Source

Check whether a given sequence is non-decreasing.

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

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.

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 `n` 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 () Source

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.