Invariant Inference Perspective

Strongest and weakest invariant, $I$, to prove that the program

s1; r*; s3

when started in a state from set $P1$ ends with a state from $Q1$.

Take $P = sp(P1,s1)$, $Q = wp(s3,Q1)$.

Hint: consider $sp(P,r^n)$ and $wp(r^n,Q)$.

Find the strongest, weakest, and a simple invariant for the Hoare triple:

assume(x > 5 && y == 0)
while (x > 0) {
  y = y + x
  x = x - 1
assert(y > 5)

So, we can go from beginning or from the end.

Or we can go faster than sp, using some $sp\#(P,r^n)$. This ensures we are above $sp\#(P,r^n)$ and then we check if we managed to prove the assertion.

Dually, we could start from some stronger $wp\#(P,r^n)$ and check if we can ensure with the precondition.

To formalize working with $sp\#$ and $wp\#$ we use monotone functions on lattices.


Let $S$ be a set (e.g. the set of all integers). Let $Init, Good \subseteq S$ and $r \subseteq S \times S$. Define

   Invs = \{ I \subseteq S \mid Init \subseteq I \land sp(I,r)\subseteq I \land I \subseteq Good \}

For each element $I \in Invs$ we have $I \subseteq S$ and we think of $I$ as an invariant. Assume $Invs \neq \emptyset$.

a): Show $sp(Init,r^*) \subseteq I$ and $I \subseteq wp(r^*, Good)$ for each $I \in Invs$.

b) Show that $\{ I \} r \{ I \}$ iff $F(I)=I$ where $F$ is a function from sets of states to sets of states, $F : 2^{S} \to S^S$ defined by

    F(I) \ = \ I \cup sp(I,r) 

Moreover, $\{ I \} r \{ I \}$ iff $G(I)=I$ for

   G(I) \ = \ I \cap wp(r,I)

c): If $I_1,I_2 \in Invs$, is $I_1 \cup I_2 \in Invs$?

d): If $I_1,I_2 \in Invs$, is $I_1 \cap I_2 \in Invs$?

e): Let $Invs1 \subseteq Invs$ and let

    J = \bigcap_{I \in Invs1} I

in other words, by definition of $\bigcap$,

   J = \{ x \mid \forall I \in Invs1.\ x \in I \}

Prove that then $J \in Invs$.

  • What do we obtain for $Invs1 = Invs$?