# Hoare triple: Loop invariant and partial correctness

Below there is Hoare triple in which variable $$a$$ is an array of integers, $$len$$, $$x, i$$ are integer-valued variables, and $$r$$ is a Boolean-valued variable. I have to provide a loop invariant (using predicate logic) suitable for proving partial correctness and explain in words why it is a loop invariant and why it is sufficient to prove partial correctness.

\begin{align*} &\{0 ≤ len \} \\ &i = 0; \\ &r = \textbf{false}; \\ &\textbf{while}\;(i < len)\;\{ \\ &\quad\textbf{if}\;(a[i] = x)\;\{ \\ &\quad\quad r = \textbf{true}; \\ &\quad\quad i = len; \\ &\quad \}\;\textbf{else}\;\{ \\ &\quad\quad i = i + 1;\\ &\quad \} \\ &\} \\ &\{(r=\textbf{true})\iff(\exists k \in \mathbb{Z}: (0 \le k \land k < len \land a[k] = x ))\} \end{align*}

I tried to use loop rule and get the invariant I by the third premise:

$$\{I \land \lnot b\} \; [] \; S \; \{Q\}$$

What I did: $$\{I \land i < len \} \implies \{(r = \textbf{true}) \iff (\exists k \in \mathbb{Z}:(0 \le k \land k < len \land a[k] = x ))\}$$

I can not go anymore at here, because I do not know how to find an invariant $$\land$$ $$a[ i ] \neq x$$ $$\implies$$ postcondition. And if $$a[ i ] \neq x$$ that means this it does not find $$x$$ in array $$a$$. But the postcondition said it will find $$x$$ because $$r = \textbf{true}$$.

• Try replacing $len$ with $i$ in the postcondition. Mar 28, 2019 at 14:14
• @dkaeae Sir, because the negative guard is i >= len, thus it already satisfy the postcondition, so I guess we only need to find an invariant which does not make the array be null is ok.
– BoiD
Mar 28, 2019 at 14:31
• I meant replacing $len$ with $i$ in the $\exists k \in \mathbb{Z}: \cdots$ part. Mar 28, 2019 at 14:38
• @dkaeae Sir, I come up with an invariant: i <= leni >= len ∧ ∃ k ∈Z:( 0 ≤ kk < ia [k] = x
– BoiD
Mar 28, 2019 at 14:46
• @BoiD A bit better: i <= len \/ i >= len /\ ... — note the or instead of the and, since your i <= len /\ i >= len gives i = len. But in fact, I’d try as invariant $r = \mathit{false} \land i \le \mathit{len} \lor r = \mathit{true} \land i = \mathit{len} \land \exists k.\, \ldots$. Depending on the flag r, our invariant gives different conditions. Apr 1, 2019 at 10:22