Mathematics for Computer Science

6.4. Strong Induction vs. Induction vs. Well Ordering 145

whiles¤ 0 do
if 3 jsthen
rWDrCrCr;
sWDs=3;
else if 3 j.s1/then
aWDaCr;
rWDrCrCr;
sWD.s1/=3;
else
aWDaCrCr;
rWDrCrCr;
sWD.s2/=3;
returna;

We can model the algorithm as a state machine whose states are triples of non-
negative integers.r;s;a/. The initial state is.x;y;0/. The transitions are given by
the rule that fors > 0:

.r;s;a/!

8

ˆ<

ˆ:

.3r;s=3;a/ if 3 js

.3r;.s1/=3;aCr/ if 3 j.s1/

.3r;.s2/=3;aC2r/ otherwise:

(a)List the sequence of steps that appears in the execution of the algorithm for
inputsxD 5 andyD 10.

(b)Use the Invariant Method to prove that the algorithm is partially correct—that
is, ifsD 0 , thenaDxy.

(c)Prove that the algorithm terminates after at most 1 Clog 3 yexecutions of the
body of thedostatement.

Problem 6.12.
A robot named Wall-E wanders around a two-dimensional grid. He starts out at
.0;0/and is allowed to take four different types of step:

1..C2;1/

2..C1;2/

3..C1;C1/