Mathematics for Computer Science

(Frankie) #1

Chapter 6 Induction132


multiplications calledFast Exponentiation. The register machine program below
defines the fast exponentiation algorithm. The lettersx;y;z;rdenote registers that
hold numbers. Anassignment statementhas the form “zWDa” and has the effect
of setting the number in registerzto be the numbera.


A Fast Exponentiation Program
Given inputsa 2 R;b 2 N, initialize registersx;y;ztoa;1;brespectively, and
repeat the following sequence of steps until termination:

 ifzD 0 returnyand terminate
 rWDremainder.z;2/
 zWDquotient.z;2/
 ifrD 1 , thenyWDxy
 xWDx^2

We claim this program always terminates and leavesyDab.
To begin, we’ll model the behavior of the program with a state machine:


  1. statesWWDRRN,

  2. start stateWWD.a;1;b/,

  3. transitions are defined by the rule


.x;y;z/!

(


.x^2 ;y;quotient.z;2// ifzis nonzero and even;
.x^2 ;xy;quotient.z;2// ifzis nonzero and odd:

The preserved invariant,P..x;y;z//, will be

z 2 NANDyxzDab: (6.4)

To prove thatPis preserved, assumeP..x;y;z//holds and that.x;y;z/!
.xt;yt;zt/. We must prove thatP..xt;yt;zt//holds, that is,


zt 2 NANDytxtztDab: (6.5)

Since there is a transition from.x;y;z/, we havez ¤ 0 , and sincez 2 N
by (6.4), we can consider just two cases:

Free download pdf