The program below, called foo, calculates zy and stores the value in r (%' is the modulo operation, e.g. 345 % 10 = 5, and '/' is integer division - division without reminder, e.g. 345 / 10 = 34): foo while (m> 0) if m%2-1 then r m :- else = r + n; 1; n := n* 2; m / 2; body (You may use the abbreviation 'body' to refer to the program inside the while loop, and 'foo' to refer to the entire program.) The goal of this exercise is to show that foo conforms to its specification, i.e. to show that the Hoare triple {(m=z) ^ (n= y) ^ (r=0)^(z 20)} foo {(r=zy)} is valid. a) Find a suitable loop invariant I. Here suitable means 1. The invariant is established: (m = z) ^ (n = y) ^ (r=0) ^ (20) I. 2. The postcondition is established: IA-b (r=2*y). 3. The invariant is invariant: (/A b)body{1}. where bm> 0 is the loop condition. State the invariant, no proof required (yet). b) Using invariant I found in (a), or otherwise, prove that {I^b)} body {1} is valid in the Hoare calculus for partial correctness. Justify each step in your proof. c) Continue the proof in (b) to prove that {(m=x) ^ (n=y) ^ (r=0) ^ (20)} foo {{(r=ry)} is valid in the Hoare calculus for partial correctness. Justify each step in your proof.