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 2 b 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