2
$\begingroup$

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

Improve this question
$\endgroup$
8
  • $\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 <= len ∧ i >= len ∧ ∃ k ∈Z:( 0 ≤ k ∧ k < i ∧ a [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$
    – Blaisorblade
    Apr 1, 2019 at 10:22

0

Reset to default

Your Answer

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