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

Documentation.SBV.Examples.ProofTools.Sum

Contents

Description

Author : Levent Erkok License : BSD3 Maintainer: erkokl@gmail.com Stability : experimental

Example inductive proof to show partial correctness of the traditional for-loop sum algorithm:

    s = 0
i = 0
while i <= n:
s += i
i++


We prove the loop invariant and establish partial correctness that s is the sum of all numbers up to and including n upon termination.

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 Fieldss :: a i :: a n :: a
Instances
 Source # Queriable 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 :: (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.Sum" "sbv-8.0-4OZZzEgTRNf59WYE3yYwTJ" False) (C1 (MetaCons "S" PrefixI True) (S1 (MetaSel (Just "s") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: (S1 (MetaSel (Just "i") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Just "n") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a))))

Encoding partial correctness of the sum algorithm. We have:

>>> sumCorrect
Q.E.D.