break, continue, return, goto

[Rick Richardson]

>   What I am worrying about is how the postcondition of a multi-exit loop
> can be EASILY recovered (I assume it is not normally documented). 
> ... MORE HYPE ... Then these examples:
  i = 0;
  /* Loop Invariant : (i <= HIGH+1) and X is not found in array[0..i-1] */
  while ( (i <= HIGH) && (array[i] <> X) {
    i++
  }       

  if (i = HIGH+1) { /* X is not found in array[0..HIGH] */
    .... not found .....
  } else { /* (i < HIGH+1) and X is not found in [0..i-1] & (array[i]=X) */
    ... found .........
  }
 
In contrast :
 
  for (i:=0; ++i; i>HIGH) 
    if (array[i] = X) {
      break 
    } 

> is less clear in the sense that the position of loop invariant is not
> obvious. Also it is less clear how the exit conditions should be treated 
> after loop termination.

If this second example is less clear than the first, then I must be getting
too old to grok whatever they are teaching in school these days.  To me,
the important part is whether the next guy (or me, 6 months later) can
understand the code.  The second example is much easier to understand than
the first.  Maybe it is harder to prove (though I'll admit I don't know),
but:
	1) So what.  I *never* run proveit(1) on my programs.
		    (anybody got a copy).
	2) Let me program what is understandable to humans.
	   If the program provers can't handle my code, that is their
	   deficiency, not mine. 
Rick Richardson
PC Research, Inc.
P.S. Your examples aren't even close to compilable 'C'.  Perhaps if you
had written some 'C' code, you might give up your religion for the *real*
world. I did.