Portability | portable |
---|---|

Stability | experimental |

Maintainer | erkokl@gmail.com |

Safe Haskell | Safe-Infered |

Symbolic implementation of merge-sort and its correctness.

# Implementing Merge-Sort

Element type of lists we'd like to sort. For simplicity, we'll just
use `SWord8`

here, but we can pick any symbolic type.

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:

`>>>`

Q.E.D.`correctness 5`

# Generating C code

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.