Python question

Question

To show that an assertion A is a loop invariant, is it enough to argue that the execution of the loop body preserves A? Justify your answer.

Answer 1

Well almost, to prove that an assertion A is a loop invariant there are specifics for ensuring that it is the case.

First you have to prove upon initialization of the loop, that the Assertion A is true. Then you can assume that the variant holds true for some arbitrary iteration -> but you have to now show that if it is true for some arbitrary iteration it must also hold true for the next iteration of the loop as well. Finally you have to show that upon termination the loop invariant still holds true as well. If you can show these, you can prove the correctness of your loop.