Mathematics for Computer Science

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: