The following transformation was found in an article on program manipulation
published in Communications of the ACM (See [1] Section 2.3.4):
do S1 od is equivalent to do S2 od
if and only if
do S1 od is equivalent to do S1; S2 od
Here, S1 and S2 are any statements and the do . . . od loops are unbounded
or infinite loops which can only be terminated by executing an exit state-
ment within the loop body. The statement exit(n) will terminate n enclosing
do . . . od loops.
The reverse implication is easily seen to be false: simply take S2 to be skip,
then for any statement S1:
do S1 od is equivalent to do S1; skip od
but:
do S1 od is not necessarily equivalent to do skip od
The forward implication looks more reasonable, and quite a useful transforma-
tion: it suggests that if we have two loops which implement the same program,
then we can generate another program by combining the two loop bodies into
a single loop.
It turns out that this is not a valid transformation!
Consider these two programs, where x is an integer variable:
Program P1 is:
do if x 6 0 then exit fi;
if even(x) then x := x − 2 else x := x + 1 fi od
Program P2 is:
do if x 6 0 then exit fi;
x := x − 1 od
Show that these two programs are equivalent.
What about the “combined” program?
Program P3 is:
do if x 6 0 then exit fi;
if even(x) then x := x − 2 else x := x + 1 fi;
if x 6 0 then exit fi;
x := x − 1 od
Is P3 equivalent to P1 and P2?
In the same paper, the author uses this “transformation” to “prove” the fol-
lowing:
do if ¬B then exit(1) fi;
do if B ^ B1 then S1 else exit(1) fi od;
do if B ^ ¬B1 then S2 else exit(1) fi od od
is equivalent to:
do if ¬B then exit(1) fi;
if B1 then S1 else S2 fi od
The statements can equivalently be expressed as while loops:
while B do
while B ^ B1 do S1 od;
while B ^ ¬B1 do S2 od od
is equivalent to:
while B do
if B1 then S1 else S2 fi od
Is this transformation valid?
Either give an informal proof of the correctness of this transformation (if you
think it is valid), or find a counterexample (if you think it is not valid).
Marking criteria:
1. Show that P1 is equivalent to P2 and determine whether P3 is also equiv-
alent to P1 and P2 (10 marks)
2. Produce a convincing argument or counterexample for the last proposed
transformation (10 marks)
