CSC236H5 Lecture Notes - Lecture 8: Precondition
Document Summary
Consider the following function: def mystery(a,b): while a>=0 and b >=0: return a if a < b: else: is not always decreasing on every iteration. If a < b, then a actually increases in the loop. only decreases in the else branch: state and prove the variant for the loop! Ans: let the variant be 2b + a. Let a_0, b_0 represent the initial values, and a_1, b_1 represent the values after one iteration. We know that a_1 = b_0 and b_1 = a_0, which means b_1 < a_1. So a0 < b0 2b0 + a0 > 2b1 + a1. Also, since a, b >=0 we know that 2b+a >=0. Let"s mess with the gcd example from lecture again. For each of the following, give a full correctness argument if the code is correct; otherwise, show where a correctness argument would fail. def gcd1(a, b): If b == 1, then gcd(a,1) = 1.
