| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Documentation.SBV.Examples.ProofTools.AddHorn
Description
Example of invariant generation for a simple addition algorithm:
z = x
i = 0
assume y > 0
while (i < y)
z = z + 1
i = i + 1
assert z == x + y
We use the Horn solver to calculate the invariant and then show that it indeed is a sufficient invariant to establish correctness.
Documentation
>>>-- For doctest purposes only:>>>import Data.SBV
type Inv = (SInteger, SInteger, SInteger, SInteger) -> SBool Source #
Helper type synonym for the invariant.
type VC = Forall "x" Integer -> Forall "y" Integer -> Forall "z" Integer -> Forall "i" Integer -> SBool Source #
Helper type synonym for verification conditions.
First verification condition: Before the loop starts, invariant must hold:
\(z = x \land i = 0 \land y > 0 \Rightarrow inv (x, y, z, i)\)
Second verification condition: If the loop body executes, invariant must still hold at the end:
\(inv (x, y, z, i) \land i < y \Rightarrow inv (x, y, z+1, i+1)\)
Third verification condition: Once the loop exits, invariant and the negation of the loop condition must establish the final assertion:
\(inv (x, y, z, i) \land i \geq y \Rightarrow z == x + y\)
synthesize :: IO SatResult Source #
Synthesize the invariant. We use an uninterpreted function for the SMT solver to synthesize. We get:
>>>synthesizeSatisfiable. Model: invariant :: (Integer, Integer, Integer, Integer) -> Bool invariant (x, y, z, i) = x + (-z) + i > (-1) && x + (-z) + i < 1 && x + y + (-z) > (-1)
This is a bit hard to read, but you can convince yourself it is equivalent to x + i .== z .&& x + y .>= z:
>>>let f (x, y, z, i) = x + (-z) + i .> (-1) .&& x + (-z) + i .< 1 .&& x + y + (-z) .> (-1)>>>let g (x, y, z, i) = x + i .== z .&& x + y .>= z>>>f === (g :: Inv)Q.E.D.