Problem 2 (15 points) Consider the following program specification: Input: a E Z, b ez Output: ab = a-a-...-a (i.e., a multiplied b times) and the following implementation: procedure QuickPower(a (1) if b 1 then return a (2) else r = QuickPowera, lb/2) (3) if b is odd then return arr (4) else return r.r Show that QuickPower correctly implements the program specification by establishing a. partial correctness and b. termination