[General boards] [Fall 2018 courses] [Summer 2018 courses] [Winter 2018 courses] [Older or newer terms]

Will we have to prove loop invariants outside of correctness?


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.