Documentation.SBV.Examples.ProofTools.AddHorn

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

type Inv = (SInteger, SInteger, SInteger, SInteger) -> SBool

Helper type synonym for the invariant.

type VC = Forall "x" Integer -> Forall "y" Integer -> Forall "z" Integer -> Forall "i" Integer -> SBool

Helper type synonym for verification conditions.

quantify :: Inv -> VC

Helper for turning an invariant predicate to a boolean.

vc1 :: Inv -> VC

First verification condition: Before the loop starts, invariant must hold:

\(z = x \land i = 0 \land y > 0 \Rightarrow inv (x, y, z, i)\)

vc2 :: Inv -> VC

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)\)

vc3 :: Inv -> VC

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

Synthesize the invariant. We use an uninterpreted function for the SMT solver to synthesize. We get:

>>> synthesize
Satisfiable. 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.

verify :: IO ThmResult

Verify that the synthesized function does indeed work. To do so, we simply prove that the invariant found satisfies all the vcs:

>>> verify
Q.E.D.