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

Documentation.SBV.Examples.TP.McCarthy91

Contents

Definitions
Correctness

Description

Proving McCarthy's 91 function correct.

Synopsis

mcCarthy91 :: SInteger -> SInteger
spec91 :: SInteger -> SInteger
correctness :: IO (Proof (Forall "n" Integer -> SBool))

Definitions

mcCarthy91 :: SInteger -> SInteger Source #

Nested recursive definition of McCarthy's function.

spec91 :: SInteger -> SInteger Source #

Specification for McCarthy's function.

Correctness

correctness :: IO (Proof (Forall "n" Integer -> SBool)) Source #

We prove the equivalence of the nested recursive definition against the spec with a case analysis and strong induction. We have:

>>> correctness
Lemma: case1                            Q.E.D.
Lemma: case2                            Q.E.D.
Inductive lemma (strong): case3
  Step: Measure is non-negative         Q.E.D.
  Step: 1 (unfold)                      Q.E.D.
  Step: 2                               Q.E.D.
  Result:                               Q.E.D.
Lemma: mcCarthy91
  Step: 1 (3 way case split)
    Step: 1.1                           Q.E.D.
    Step: 1.2                           Q.E.D.
    Step: 1.3                           Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
[Proven] mcCarthy91 :: Ɐn ∷ Integer → Bool