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


#1

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?


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