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.

Exercise

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

$\begin{equation*} Invs = \{ I \subseteq S \mid Init \subseteq I \land sp(I,r)\subseteq I \land I \subseteq Good \} \end{equation*}$

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

$\begin{equation*} F(I) \ = \ I \cup sp(I,r) \end{equation*}$

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

$\begin{equation*} G(I) \ = \ I \cap wp(r,I) \end{equation*}$

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

$\begin{equation*} J = \bigcap_{I \in Invs1} I \end{equation*}$

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

$\begin{equation*} J = \{ x \mid \forall I \in Invs1.\ x \in I \} \end{equation*}$

Prove that then $J \in Invs$ .

What do we obtain for $Invs1 = Invs$ ?