break, et cetera

[Chris Torek]

Darn...  when I got up this evening I realized that I had not really
said what I wanted to in the first part of that article.  I hate
to reopen the wound and rub in salt, but . . . here goes:

Given a C construct such as

	for (init; cond; step) {
		code;
		if (cond2)
			break;
		code2;
	}

one can, without changing the meaning of the code, write

	init;
	bool := true;
	while (cond) and bool do
	   begin code;
	   if cond2 then
	      bool := false
	   else
	      begin code2;
	      step
	      end
	   end;

which is how the loop would most likely appear in Pascal.  (The
expanded form if `code' or `code2' contains `continue' statements
is somewhat different, but does exist.)  This expanded form can be
transformed direcly into C in the obvoius way.

These are semantically equivalent when it comes to proving the code
correct.  Since they are equivalent, you may elect to use either
form.  In C, I would use the `compressed' form; but this is a matter
of taste, and you probably know the old expression concerning such.
-- 
In-Real-Life: Chris Torek, Univ of MD Comp Sci Dept (+1 301 454 4251)
UUCP:	seismo!umcp-cs!chris
CSNet:	chris at umcp-cs		ARPA:	chris at mimsy.umd.edu