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}$.

  • $\begingroup$ Try replacing $len$ with $i$ in the postcondition. $\endgroup$
    – dkaeae
    Mar 28, 2019 at 14:14
  • $\begingroup$ @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. $\endgroup$
    – BoiD
    Mar 28, 2019 at 14:31
  • $\begingroup$ I meant replacing $len$ with $i$ in the $\exists k \in \mathbb{Z}: \cdots$ part. $\endgroup$
    – dkaeae
    Mar 28, 2019 at 14:38
  • $\begingroup$ @dkaeae Sir, I come up with an invariant: i <= leni >= len ∧ ∃ k ∈Z:( 0 ≤ kk < ia [k] = x $\endgroup$
    – BoiD
    Mar 28, 2019 at 14:46
  • $\begingroup$ @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. $\endgroup$ Apr 1, 2019 at 10:22


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.