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$
  • $\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$ – David Richerby Mar 20 '18 at 9:43
  • $\begingroup$ The invariant expresses that the array copy has been partially performed. $\endgroup$ – Yves Daoust Mar 20 '18 at 10:57
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$
  • 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$ – Musa Al-hassy Mar 20 '18 at 11:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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