Consider the following program specification: input: a e Z, b e Z+ Output: ab -aaa (i.e., a multiplied b times) and the following implementation: procedure RapidPower(a, b) (1) if b- 1 then return a (2) else r-RapidPower(a, Lb/2]) (3) if b is odd then return a-r.r (4) else return rr Show that RapidPower correctly implements the program specification by establishing a. partial correctness and b. termination