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

Copyright (c) Levent Erkok BSD3 erkokl@gmail.com experimental None Haskell2010

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.