Data.SBV.Plugin.Examples.MergeSort

An implementation of merge-sort and its correctness.

Implementing merge-sort

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

merge :: Ord a => [a] -> [a] -> [a]

Merging two given sorted lists, preserving the order.

mergeSort :: Ord a => [a] -> [a]

Simple merge-sort implementation.

Proving correctness of sorting

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 :: Ord a => [a] -> Bool

Check whether a given sequence is non-decreasing.

isPermutationOf :: Eq a => [a] -> [a] -> Bool

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.

The correctness theorem

mergeSortCorrect :: [Int] -> Bool

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. Here we try it with 4.

We have:

  [SBV] tests/T48.hs:100:1-16 Proving "mergeSortCorrect", using Z3.
  [Z3] Q.E.D.