Copyright | (c) Levent Erkok |
---|---|
License | BSD3 |
Maintainer | erkokl@gmail.com |
Stability | experimental |
Safe Haskell | None |
Language | Haskell2010 |
Documentation.SBV.Examples.ProofTools.Fibonacci
Contents
Description
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.
Synopsis
- data S a = S {}
- fibCorrect :: IO (InductionResult (S Integer))
System state
System state. We simply have two components, parameterized over the type so we can put in both concrete and symbolic values.
Instances
Functor S Source # | |
Foldable S Source # | |
Defined in Documentation.SBV.Examples.ProofTools.Fibonacci Methods foldMap :: Monoid m => (a -> m) -> S a -> m foldMap' :: Monoid m => (a -> m) -> S a -> m foldr :: (a -> b -> b) -> b -> S a -> b foldr' :: (a -> b -> b) -> b -> S a -> b foldl :: (b -> a -> b) -> b -> S a -> b foldl' :: (b -> a -> b) -> b -> S a -> b foldr1 :: (a -> a -> a) -> S a -> a foldl1 :: (a -> a -> a) -> S a -> a | |
Traversable S Source # | |
Fresh IO (S SInteger) Source # |
|
Show a => Show (S a) Source # | |
Generic (S a) Source # | |
Mergeable a => Mergeable (S a) Source # | |
type Rep (S a) Source # | |
Defined in Documentation.SBV.Examples.ProofTools.Fibonacci type Rep (S a) = D1 ('MetaData "S" "Documentation.SBV.Examples.ProofTools.Fibonacci" "sbv-8.6-5LFzpcwNP9O6D9gqHorKOG" '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)) Source #
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!