Consider the following program specification:

Input: a in $,$ b in $+$

Output: ab $=$ a$$a$...$a $($i$.$e$.,$ a multiplied b times$)$

and the following implementation:

$$procedure QuickPower$($a$,$ b$)(1)$if b $=1$ then return a$(2)$else r $=$ QuickPower$($a$,$b$/2)(3)$if b is odd then return a$$r$$r$(4)$else return r$$r

Show that QuickPower correctly implements the program specification by establishing

partial correctness and

termination

See Program Correctness Overview Download Program Correctness Overview$$for the procedure you must use for proving partial correctness and termination for a recursive program as well as this example of proving program correctness for recursive programs