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

Documentation.SBV.Examples.TP.BinarySearch

Contents

Binary search
Correctness proof

Description

Proving binary search correct

Synopsis

type Arr = SArray Integer Integer
type Idx = (SInteger, SInteger)
bsearch :: Arr -> Idx -> SInteger -> SMaybe Integer
nonDecreasing :: Arr -> Idx -> SBool
inArray :: Arr -> Idx -> SInteger -> SBool
correctness :: IO (Proof (Forall "arr" (ArrayModel Integer Integer) -> Forall "lo" Integer -> Forall "hi" Integer -> Forall "x" Integer -> SBool))

Binary search

type Arr = SArray Integer Integer Source #

We will work with arrays containing integers, indexed by integers. Note that since SMTLib arrays are indexed by their entire domain, we explicitly take a lower/upper bounds as parameters, which fits well with the binary search algorithm.

type Idx = (SInteger, SInteger) Source #

Bounds: This is the focus into the array; both indexes are inclusive.

bsearch :: Arr -> Idx -> SInteger -> SMaybe Integer Source #

Encode binary search in a functional style.

Correctness proof

nonDecreasing :: Arr -> Idx -> SBool Source #

A predicate testing whether a given array is non-decreasing in the given range

inArray :: Arr -> Idx -> SInteger -> SBool Source #

A predicate testing whether an element is in the array within the given bounds

correctness :: IO (Proof (Forall "arr" (ArrayModel Integer Integer) -> Forall "lo" Integer -> Forall "hi" Integer -> Forall "x" Integer -> SBool)) Source #

Correctness of binary search.

We have:

>>> correctness
Lemma: notInRange                                 Q.E.D.
Lemma: inRangeHigh                                Q.E.D.
Lemma: inRangeLow                                 Q.E.D.
Lemma: nonDecreasing                              Q.E.D.
Inductive lemma (strong): bsearchAbsent
  Step: Measure is non-negative                   Q.E.D.
  Step: 1 (unfold bsearch)                        Q.E.D.
  Step: 2 (push isNothing down, simplify)         Q.E.D.
  Step: 3 (2 way case split)
    Step: 3.1                                     Q.E.D.
    Step: 3.2.1                                   Q.E.D.
    Step: 3.2.2                                   Q.E.D.
    Step: 3.2.3                                   Q.E.D.
    Step: 3.2.4                                   Q.E.D.
    Step: 3.2.5 (simplify)                        Q.E.D.
    Step: 3.Completeness                          Q.E.D.
  Result:                                         Q.E.D.
Inductive lemma (strong): bsearchPresent
  Step: Measure is non-negative                   Q.E.D.
  Step: 1 (unfold bsearch)                        Q.E.D.
  Step: 2 (simplify)                              Q.E.D.
  Step: 3 (3 way case split)
    Step: 3.1                                     Q.E.D.
    Step: 3.2                                     Q.E.D.
    Step: 3.3.1                                   Q.E.D.
    Step: 3.3.2 (3 way case split)
      Step: 3.3.2.1                               Q.E.D.
      Step: 3.3.2.2.1                             Q.E.D.
      Step: 3.3.2.2.2                             Q.E.D.
      Step: 3.3.2.3.1                             Q.E.D.
      Step: 3.3.2.3.2                             Q.E.D.
      Step: 3.3.2.Completeness                    Q.E.D.
    Step: 3.Completeness                          Q.E.D.
  Result:                                         Q.E.D.
Lemma: bsearchCorrect
  Step: 1 (2 way case split)
    Step: 1.1.1                                   Q.E.D.
    Step: 1.1.2                                   Q.E.D.
    Step: 1.2.1                                   Q.E.D.
    Step: 1.2.2                                   Q.E.D.
    Step: 1.Completeness                          Q.E.D.
  Result:                                         Q.E.D.
[Proven] bsearchCorrect :: Ɐarr ∷ (ArrayModel Integer Integer) → Ɐlo ∷ Integer → Ɐhi ∷ Integer → Ɐx ∷ Integer → Bool