Assume that some processor (which uses multiplication very seldom and must use as less energy as possible) does not have hardware implementation of multipli- cation. Instead, when needed, it uses the following procedure (written in an easily understood pseudocode, for easier proof of correctness): procedure multiply(m.n : integers, return product: integers) if n < 0 then a := -n else a:= n; k:= 0; x := 0; while k < a do begin x :=x+m;k :=k+1; end; if n < 0 then product := -x else product :=x end of procedure Prove the correctness (i.e. product = m - n) and termination using Hoare triples.