Question

For an algorithm, what is the likely relationship between a loop invariant and a postcondition?

Answer 1

For an algorithm,postcondition is a statement placed after end of the segment that should be true when the execution of segment is complete.An invarient is a statement placed in a code segment that should be true each time the loop execution reaches that point.

In the loop invariant, assertion supposed to be true before and after the each iteration of the loop

If the precondition is true, then postcondition will be true.

If the invariant is placed at the beginning of a while or do-while loop whose condition test does not change the state of the computation (i.e; no side effects), then the invariant should also be true at the bottom of the loop.