Documentation.SBV.Examples.ProofTools.Fibonacci

Author : Levent Erkok License : BSD3 Maintainer: [e-mail] Stability : experimental

Example inductive proof to show partial correctness of the for-loop based fibonacci algorithm:

    i = 0
    k = 1
    m = 0
    while i < n:
       m, k = k, m + k
       i++

We do the proof against an axiomatized fibonacci implementation using an uninterpreted function.

System state

data S a

System state. We simply have two components, parameterized over the type so we can put in both concrete and symbolic values.

Constructors

S

Fields

• i :: a
• k :: a
• m :: a
• n :: a

Instances

Queriable IO (S SInteger) (S Integer)

Make our state queriable

Defined in Documentation.SBV.Examples.ProofTools.Fibonacci

Methods

fresh :: QueryT IO (S SInteger)

extract :: S SInteger -> QueryT IO (S Integer)

Show a => Show (S a)

Defined in Documentation.SBV.Examples.ProofTools.Fibonacci

Methods

showsPrec :: Int -> S a -> ShowS

show :: S a -> String

showList :: [S a] -> ShowS

Generic (S a)

Defined in Documentation.SBV.Examples.ProofTools.Fibonacci

Associated Types

type Rep (S a) :: Type -> Type

Methods

from :: S a -> Rep (S a) x

to :: Rep (S a) x -> S a

Mergeable a => Mergeable (S a)

Defined in Documentation.SBV.Examples.ProofTools.Fibonacci

Methods

symbolicMerge :: Bool -> SBool -> S a -> S a -> S a

select :: (SymVal b, Num b) => [S a] -> S a -> SBV b -> S a

type Rep (S a)

Defined in Documentation.SBV.Examples.ProofTools.Fibonacci

type Rep (S a) = D1 (MetaData "S" "Documentation.SBV.Examples.ProofTools.Fibonacci" "sbv-8.0-4OZZzEgTRNf59WYE3yYwTJ" False) (C1 (MetaCons "S" PrefixI True) ((S1 (MetaSel (Just "i") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Just "k") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a)) :*: (S1 (MetaSel (Just "m") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Just "n") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a))))

fibCorrect :: IO (InductionResult (S Integer))

Encoding partial correctness of the sum algorithm. We have:

>>> fibCorrect
Q.E.D.

NB. In my experiments, I found that this proof is quite fragile due to the use of quantifiers: If you make a mistake in your algorithm or the coding, z3 pretty much spins forever without finding a counter-example. However, with the correct coding, the proof is almost instantaneous!