Techniques for Automated Deduction

... WP(s, B) I holds on entry I is preserved in an arbitrary iteration B holds when the loop terminates if Ik = return S(Postcurrent) if Ik = x : ...