Symbolic implementation of merge-sort and its correctness.
Element type of lists we'd like to sort. For simplicity, we'll just
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.
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
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:
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.