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?
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.