Reference no: EM131981499

To express a general rule for proving correctness of a "while" loop, we used the concept of a loop invariant. Which of the following informal conditions does NOT need to hold of a loop invariant for that rule to apply?

A. The overall precondition implies the loop invariant

B. The loop invariant implies that the loop test expression is true

C. Whenever the loop test expression is true, running the loop body preserves the loop invariant

D. Whenever the loop test expression is false, the loop invariant implies the overall postcondition