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

Safe HaskellNone




Symbolic implementation of merge-sort and its correctness.


Implementing Merge-Sort

type E = SWord8Source

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

Check whether a given sequence is non-decreasing.

isPermutationOf :: [E] -> [E] -> SBoolSource

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 ThmResultSource

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

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 it's Haskell counterpart.