3. Give a full proof outline (under partial correctness) obtained by expansion of the partial proof outline below. Use backward assignment whenever possible. Give a brief explanation on each logical implication used in the proof. {y 1} x = 0; r = 1; {inv p=1r = 2x y} while 2 * r < y do r = 2 *r; x = x + 1 od {r2 y 2x+1} = 4. Solve Question 3 again but use forward assignment whenever possible this time. 5. Find a reasonable bound expression for the loop in Question 3, then create a full proof outline under total correctness by expansion of your full proof outline given in Question 3 (the one you use backward assignment everywhere).