sbv-11.4: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Documentation.SBV.Examples.KnuckleDragger.MergeSort

Description

Proving merge-sort correct.

Synopsis

Merge sort

merge :: SList Integer -> SList Integer -> SList Integer Source #

Merge two already sorted lists into another

mergeSort :: SList Integer -> SList Integer Source #

Merge sort, using merge above to successively sort halved input

Helper functions

nonDecreasing :: SList Integer -> SBool Source #

A predicate testing whether a given list is non-decreasing.

count :: SInteger -> SList Integer -> SInteger Source #

Count the number of occurrences of an element in a list

isPermutation :: SList Integer -> SList Integer -> SBool Source #

Are two lists permutations of each other?

Correctness proof

correctness :: IO Proof Source #

Correctness of merge-sort.

We have:

>>> correctness
Lemma: nonDecrInsert                              Q.E.D.
Lemma: nonDecTail                                 Q.E.D.
Inductive lemma (strong): mergeKeepsSort
  Base: mergeKeepsSort.Base                       Q.E.D.
  Step: 1                                         Q.E.D.
  Step: 2                                         Q.E.D.
  Asms: 3                                         Q.E.D.
  Step: 3                                         Q.E.D.
  Asms: 4                                         Q.E.D.
  Step: 4                                         Q.E.D.
  Asms: 5                                         Q.E.D.
  Step: 5                                         Q.E.D.
  Asms: 6                                         Q.E.D.
  Step: 6                                         Q.E.D.
  Step: 7                                         Q.E.D.
  Step: mergeKeepsSort.Step                       Q.E.D.
Inductive lemma (strong): sortNonDecreasing
  Base: sortNonDecreasing.Base                    Q.E.D.
  Step: 1                                         Q.E.D.
  Step: 2                                         Q.E.D.
  Step: 3                                         Q.E.D.
  Step: 4                                         Q.E.D.
  Step: sortNonDecreasing.Step                    Q.E.D.
Inductive lemma (strong): mergeCount
  Base: mergeCount.Base                           Q.E.D.
  Step: 1                                         Q.E.D.
  Step: 2                                         Q.E.D.
  Step: 3                                         Q.E.D.
  Step: 4                                         Q.E.D.
  Step: 5                                         Q.E.D.
  Step: 6                                         Q.E.D.
  Step: 7                                         Q.E.D.
  Step: mergeCount.Step                           Q.E.D.
Inductive lemma: countAppend
  Base: countAppend.Base                          Q.E.D.
  Step: 1                                         Q.E.D.
  Step: 2                                         Q.E.D.
  Step: 3                                         Q.E.D.
  Step: 4                                         Q.E.D.
  Step: countAppend.Step                          Q.E.D.
Lemma: take_drop                                  Q.E.D.
Lemma: takeDropCount
  Step  : 1                                       Q.E.D.
  Step  : 2                                       Q.E.D.
  Result:                                         Q.E.D.
Inductive lemma (strong): sortIsPermutation
  Base: sortIsPermutation.Base                    Q.E.D.
  Step: 1                                         Q.E.D.
  Step: 2                                         Q.E.D.
  Step: 3                                         Q.E.D.
  Step: 4                                         Q.E.D.
  Step: 5                                         Q.E.D.
  Step: 6                                         Q.E.D.
  Step: sortIsPermutation.Step                    Q.E.D.
Lemma: mergeSortIsCorrect                         Q.E.D.
[Proven] mergeSortIsCorrect