Doing past finals, there are often times when you’re simply asked to prove that a given loop invariant holds, rather than prove partial correctness using a loop invariant. What steps do we need to take if we just want to show that a loop invariant holds? Do we just have to show the loop invariant is established and maintained, and we don’t need to worry about what happens when it terminates?

# Will we have to prove loop invariants outside of correctness?

**lettedan**#2

What you said seems correct. However, I doubt we will be asked to prove a loop invariant outside of the context of a proof of correctness. Just to be safe though, I would also show that LI + exit condition implies postcondition.