Copyright  (c) Levent Erkok 

License  BSD3 
Maintainer  erkokl@gmail.com 
Stability  experimental 
Safe Haskell  None 
Language  Haskell2010 
Example inductive proof to show partial correctness of the traditional forloop 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
 data S a = S {}
 sumCorrect :: 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.Sum fold :: 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 # elem :: Eq a => a > S a > Bool # maximum :: Ord 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.Sum type Rep (S a) = D1 (MetaData "S" "Documentation.SBV.Examples.ProofTools.Sum" "sbv8.1KJ81LMQmRNq7C7R4pcgIua" 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)))) 
sumCorrect :: IO (InductionResult (S Integer)) Source #
Encoding partial correctness of the sum algorithm. We have:
>>>
sumCorrect
Q.E.D.