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])}
Improve this question
$\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$
    – David Richerby
    Mar 20, 2018 at 9:43
  • $\begingroup$ The invariant expresses that the array copy has been partially performed. $\endgroup$
    – user16034
    Mar 20, 2018 at 10:57

1 Answer 1

Reset to default
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.

Improve this answer
$\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$
    – Musa Al-hassy
    Mar 20, 2018 at 11:40

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.

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