1. Consider the statements below, where the variables m and n are assumed to have integer values, with n > 0, and let W denote the while-loop in these statements. a := m; b:= n; c:= 0; while b>0 do if 2b then a := 2a; b:=b/2; else C:= c+a; b:=b-1; fi; od; (a) (30p) Prove that ab + c = mn is a loop invariant for W. (b) (10p) Must W terminate? Why? What is the value of b on this termination? (C) (10p) Show that on the termination of W, we have that c = mn