sbv-8.14: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Documentation.SBV.Examples.WeakestPreconditions.Fib

Description

Proof of correctness of an imperative fibonacci algorithm, using weakest preconditions. Note that due to the recursive nature of fibonacci, we cannot write the spec directly, so we use an uninterpreted function and proper axioms to complete the proof.

Synopsis

Program state

data FibS a Source #

The state for the sum program, parameterized over a base type a.

Constructors

FibS 

Fields

  • n :: a

    The input value

  • i :: a

    Loop counter

  • k :: a

    tracks fib (i+1)

  • m :: a

    tracks fib i

Instances

Instances details
Functor FibS Source # 
Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.Fib

Methods

fmap :: (a -> b) -> FibS a -> FibS b #

(<$) :: a -> FibS b -> FibS a #

Foldable FibS Source # 
Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.Fib

Methods

fold :: Monoid m => FibS m -> m #

foldMap :: Monoid m => (a -> m) -> FibS a -> m #

foldMap' :: Monoid m => (a -> m) -> FibS a -> m #

foldr :: (a -> b -> b) -> b -> FibS a -> b #

foldr' :: (a -> b -> b) -> b -> FibS a -> b #

foldl :: (b -> a -> b) -> b -> FibS a -> b #

foldl' :: (b -> a -> b) -> b -> FibS a -> b #

foldr1 :: (a -> a -> a) -> FibS a -> a #

foldl1 :: (a -> a -> a) -> FibS a -> a #

toList :: FibS a -> [a] #

null :: FibS a -> Bool #

length :: FibS a -> Int #

elem :: Eq a => a -> FibS a -> Bool #

maximum :: Ord a => FibS a -> a #

minimum :: Ord a => FibS a -> a #

sum :: Num a => FibS a -> a #

product :: Num a => FibS a -> a #

Traversable FibS Source # 
Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.Fib

Methods

traverse :: Applicative f => (a -> f b) -> FibS a -> f (FibS b) #

sequenceA :: Applicative f => FibS (f a) -> f (FibS a) #

mapM :: Monad m => (a -> m b) -> FibS a -> m (FibS b) #

sequence :: Monad m => FibS (m a) -> m (FibS a) #

SymVal a => Fresh IO (FibS (SBV a)) Source #

Fresh instance for the program state

Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.Fib

Methods

fresh :: QueryT IO (FibS (SBV a)) Source #

Show a => Show (FibS a) Source # 
Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.Fib

Methods

showsPrec :: Int -> FibS a -> ShowS #

show :: FibS a -> String #

showList :: [FibS a] -> ShowS #

(SymVal a, Show a) => Show (FibS (SBV a)) Source #

Show instance for FibS. The above deriving clause would work just as well, but we want it to be a little prettier here, and hence the OVERLAPS directive.

Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.Fib

Methods

showsPrec :: Int -> FibS (SBV a) -> ShowS #

show :: FibS (SBV a) -> String #

showList :: [FibS (SBV a)] -> ShowS #

Generic (FibS a) Source # 
Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.Fib

Associated Types

type Rep (FibS a) :: Type -> Type #

Methods

from :: FibS a -> Rep (FibS a) x #

to :: Rep (FibS a) x -> FibS a #

Mergeable a => Mergeable (FibS a) Source # 
Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.Fib

Methods

symbolicMerge :: Bool -> SBool -> FibS a -> FibS a -> FibS a Source #

select :: (Ord b, SymVal b, Num b) => [FibS a] -> FibS a -> SBV b -> FibS a Source #

type Rep (FibS a) Source # 
Instance details

Defined in Documentation.SBV.Examples.WeakestPreconditions.Fib

type Rep (FibS a) = D1 ('MetaData "FibS" "Documentation.SBV.Examples.WeakestPreconditions.Fib" "sbv-8.14-15M8sp7rKYE8iwne1Q2gA" 'False) (C1 ('MetaCons "FibS" 'PrefixI 'True) ((S1 ('MetaSel ('Just "n") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: 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))))

type F = FibS SInteger Source #

Helper type synonym

The algorithm

algorithm :: Stmt F Source #

The imperative fibonacci algorithm:

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

When the loop terminates, m contains fib(n).

fib :: SInteger -> SInteger Source #

Symbolic fibonacci as our specification. Note that we cannot really implement the fibonacci function since it is not symbolically terminating. So, we instead uninterpret and axiomatize it below.

NB. The concrete part of the definition is only used in calls to traceExecution and is not needed for the proof. If you don't need to call traceExecution, you can simply ignore that part and directly uninterpret.

axiomatizeFib :: Symbolic () Source #

Constraints and axioms we need to state explicitly to tell the SMT solver about our specification for fibonacci.

pre :: F -> SBool Source #

Precondition for our program: n must be non-negative.

post :: F -> SBool Source #

Postcondition for our program: m = fib n

noChange :: Stable F Source #

Stability condition: Program must leave n unchanged.

imperativeFib :: Program F Source #

A program is the algorithm, together with its pre- and post-conditions.

Correctness

correctness :: IO (ProofResult (FibS Integer)) Source #

With the axioms in place, it is trivial to establish correctness:

>>> correctness
Total correctness is established.
Q.E.D.

Note that I found this proof to be quite fragile: If you do not get the algorithm right or the axioms aren't in place, z3 simply goes to an infinite loop, instead of providing counter-examples. Of course, this is to be expected with the quantifiers present.

Concrete execution

 

Example concrete run. As we mentioned in the definition for fib, the concrete-execution function cannot deal with uninterpreted functions and axioms for obvious reasons. In those cases we revert to the concrete definition. Here's an example run:

>>> traceExecution imperativeFib $ FibS {n = 3, i = 0, k = 0, m = 0}
*** Precondition holds, starting execution:
  {n = 3, i = 0, k = 0, m = 0}
===> [1.1] Assign
  {n = 3, i = 0, k = 1, m = 0}
===> [1.2] Conditional, taking the "then" branch
  {n = 3, i = 0, k = 1, m = 0}
===> [1.2.1] Skip
  {n = 3, i = 0, k = 1, m = 0}
===> [1.3] Loop "i < n": condition holds, executing the body
  {n = 3, i = 0, k = 1, m = 0}
===> [1.3.{1}.1] Assign
  {n = 3, i = 0, k = 1, m = 1}
===> [1.3.{1}.2] Assign
  {n = 3, i = 1, k = 1, m = 1}
===> [1.3] Loop "i < n": condition holds, executing the body
  {n = 3, i = 1, k = 1, m = 1}
===> [1.3.{2}.1] Assign
  {n = 3, i = 1, k = 2, m = 1}
===> [1.3.{2}.2] Assign
  {n = 3, i = 2, k = 2, m = 1}
===> [1.3] Loop "i < n": condition holds, executing the body
  {n = 3, i = 2, k = 2, m = 1}
===> [1.3.{3}.1] Assign
  {n = 3, i = 2, k = 3, m = 2}
===> [1.3.{3}.2] Assign
  {n = 3, i = 3, k = 3, m = 2}
===> [1.3] Loop "i < n": condition fails, terminating
  {n = 3, i = 3, k = 3, m = 2}
*** Program successfully terminated, post condition holds of the final state:
  {n = 3, i = 3, k = 3, m = 2}
Program terminated successfully. Final state:
  {n = 3, i = 3, k = 3, m = 2}

As expected, fib 3 is 2.