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.
{0 ≤ len }
i = 0;
r = false;
while (i < len) {
if(a[i] = x){
r = true;
i = len;
}else{
i = i + 1
}
}
{(r = true) ⇔ (∃ k : Z · (0 ≤ k ∧ k < len ∧ a[k] = x ))}
I tried to use loop rule and get the invariant I by the third premise:
{I∧¬ b} [] S {Q}
What I did:
{I∧i < len} ⇒ {(r = true) ⇔ (∃ k : Z · (0 ≤ k ∧ k < len ∧ a[k] = x ))}
I can not go anymore at here, because the postcondition is a tautology, I do not know how to find an invariant.