sbv-8.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

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

# System state

data S a Source #

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

Constructors

 S Fieldsi :: a k :: a m :: a n :: a
Instances
 Source # Instance details Methodsfmap :: (a -> b) -> S a -> S b #(<\$) :: a -> S b -> S a # Source # Instance details Methodsfold :: Monoid m => S m -> 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 #toList :: S a -> [a] #null :: S a -> Bool #length :: S a -> Int #elem :: Eq a => a -> S a -> Bool #maximum :: Ord a => S a -> a #minimum :: Ord a => S a -> a #sum :: Num a => S a -> a #product :: Num a => S a -> a # Source # Instance details Methodstraverse :: Applicative f => (a -> f b) -> S a -> f (S b) #sequenceA :: Applicative f => S (f a) -> f (S a) #mapM :: Monad m => (a -> m b) -> S a -> m (S b) #sequence :: Monad m => S (m a) -> m (S a) # Source # Fresh instance for our state Instance details Methods Show a => Show (S a) Source # Instance details MethodsshowsPrec :: Int -> S a -> ShowS #show :: S a -> String #showList :: [S a] -> ShowS # Generic (S a) Source # Instance details Associated Typestype Rep (S a) :: Type -> Type # Methodsfrom :: S a -> Rep (S a) x #to :: Rep (S a) x -> S a # Mergeable a => Mergeable (S a) Source # Instance details MethodssymbolicMerge :: Bool -> SBool -> S a -> S a -> S a Source #select :: (Ord b, SymVal b, Num b) => [S a] -> S a -> SBV b -> S a Source # type Rep (S a) Source # Instance details type Rep (S a) = D1 (MetaData "S" "Documentation.SBV.Examples.ProofTools.Fibonacci" "sbv-8.2-BpcWyxFKVuJBXlUtpLk21" 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))))

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!