Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: Notesfiles; site iuvax.UUCP
Path: utzoo!watmath!clyde!cbosgd!ihnp4!inuxc!iubugs!iuvax!cjl
From: cjl@iuvax.UUCP
Newsgroups: net.lang.c
Subject: Re: break, continue, return, goto
Message-ID: <9500030@iuvax.UUCP>
Date: Thu, 14-Nov-85 20:32:00 EST
Article-I.D.: iuvax.9500030
Posted: Thu Nov 14 20:32:00 1985
Date-Received: Mon, 18-Nov-85 05:15:05 EST
References: <771@whuxl.UUCP>
Lines: 80
Nf-ID: #R:whuxl:-77100:iuvax:9500030:000:3769
Nf-From: iuvax!cjl    Nov 14 20:32:00 1985



> ..................... Well, && and || are much more of a pain to prove
> right in code than Pascal-is and/or, and assignments in expressions
> wreak havoc.  But I'm trying to write a program, not a thesis.

  A block of codes is considered structured and simple if it has a simple
precondition and postcondition formally or informally. So I agree that break
and continue could form a structured loop if they are appropriately used.
                                                          
  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). Semantically
we need a loop invariant (normally implied) before the exit point plus the
exit condition to assert the post-loop condition.   Most multi-exit loops 
I saw can be syntactically written as a single exit loop with 
conditional boolean expression (or a multi-exit loop with nested exitif
statements like 'exit when' in Ada). To me syntactic grouping of 
all exit conditions is important because it enforces ONE clear synchronization 
point for the (implied) loop invariant. Whenever loop exit points are
scattering around, the loop invariant is harder to find. Or we may even
have to assert many loop invariants for these exit points. 

  The use of conditional boolean exit conditions also reminds me to
eliminates them after terminating the loop because they are hard to
carry on in pure (non-ordered) boolean reasoning(e.g. not commutative). 
To eliminate the conditional boolean expression, we recover it to
their original if statement form. For example :

  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.
  In general it is too complex to reason, thus to design, a loop with 
general random exit points. Most multi-exit loops we face today are in
a restricted form. So why don't we impose a restriction on the use of
multi-exit loops ? The introduction of boolean expression and single
exit loop is one approach to impose a style on disciplined uses of 
multi-exit loops.  One can find other equivalent forms as well.

    Above is an example of using pure computer science theory
to judge the complexity of multi-exit loops. I'll to glad to find
different situations where reasoning multi-exit loops is easy.
        
> Can anyone suggest a recoding of the following example without using
> multiple returns?  Of course it can be done, but in a clearer, simpler
> way?  Remember, this is exactly the same as using loops with continue.

  It all depends on what postcondition you want to assert after procedure
termination. For this example, the return implies "abort". No serious
assertion  on the postcondition is considered as necessary. 
  But for other procedures it will be less clear what the post condition
is if multi-return is used. In the procedure environment, this problem
could be less serious because normally the pre- and postconditions are 
explicitly documented. We don't rely heavily on the multi-return
condition to draw the postcondition. If we ever think and document
the postcondition of our multi-exit loop in a similar serious way like
we write procedures, the problem will be less serious.


C.J.Lo
ARPA : cjl@Indiana@CSNet-Relay
UUCP : ...!iuvax!cjl