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

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Documentation.SBV.Examples.BitPrecise.MergeSort

Contents

- Implementing Merge-Sort
- Proving correctness
- Generating C code

Description

Symbolic implementation of merge-sort and its correctness.

Synopsis

- type E = SWord8
- merge :: [E] -> [E] -> [E]
- mergeSort :: [E] -> [E]
- nonDecreasing :: [E] -> SBool
- isPermutationOf :: [E] -> [E] -> SBool
- correctness :: Int -> IO ThmResult
- codeGen :: Int -> IO ()

# 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.

correctness :: Int -> IO ThmResult Source #

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 the list size 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.