I assume the term was not precisely defined neither in the lecture nor in the text book (acturally I do not see the term in there)
however, from the lecture notes, I derived the definition as:
"the loop invariant satisfy the following conditions: LI is true upon first entry to the loop; LI's true after every iteration of the loop; and LI's true after the loop exits.
MORE IMPORTANTLY, the LI, along with the fact that n=0 upon exiting the loop implies that the postcondition is true"
the extra emphasis illustrated from this descriptive definition would let me believe a constant Boolean value "true" should not be taken as a Loop invariant as it has no power to imply whether the postcondition could hold or not upon loop exit, even though of course "true"(a constant) satisfies the former three requirements.
what do people there think?
|