2
$\begingroup$

I don't know how to find a loop invariant. I'm not sure where to start. Can anyone find the loop invariant of the given program and explain your method please.

{n ≥ 0 ∧ i = 0}
while i < n − 1 loop
b[i] := a[i + 1];
i:=i + 1
end loop
{∀j.(0 ≤ j < n − 1 → b[j] = a[j + 1])}
$\endgroup$
2
  • $\begingroup$ What did you try? Where did you get stuck? If you don't know where to start, that usually means you need to go back and review your lecture notes. $\endgroup$ Commented Mar 20, 2018 at 9:43
  • $\begingroup$ The invariant expresses that the array copy has been partially performed. $\endgroup$
    – user16034
    Commented Mar 20, 2018 at 10:57

1 Answer 1

5
$\begingroup$

At the end of each iteration you have $$ \forall j: 0 \leq j < i \implies b[j] = a[j+1] $$ which you can prove by induction. Thus, when the algorithm terminates, $i$ has reached $n-1$ and you have $$ \forall j: 0 \leq j < n-1 \implies b[j] = a[j+1]\,. $$

I figured this out by just asking myself what kind of statement I can make at the end of each iteration. In this case it's that the first $i$ elements have been copied. Then I just turned that into a formal statement.

$\endgroup$
1
  • 2
    $\begingroup$ In general if you are trying to end up with post-condition R(n) then at the end of each iteration you may have R(i) ;-) $\endgroup$ Commented Mar 20, 2018 at 11:40

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.