Safe Haskell | None |
---|---|
Language | Haskell2010 |
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
- 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
Queriable IO (S SInteger) (S Integer) Source # | Queriable instance for our state |
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" "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)))) |
sumCorrect :: IO (InductionResult (S Integer)) Source #
Encoding partial correctness of the sum algorithm. We have:
>>>
sumCorrect
Q.E.D.