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 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
sumCorrect :: IO (InductionResult (S Integer)) Source #
Encoding partial correctness of the sum algorithm. We have:
>>>
sumCorrect
Q.E.D.