NetNews Usenet Archive 1992 #26/NN_1992_26.iso/spool/comp/programm/3114

Text File | 1992-11-11 | 6.3 KB | 156 lines

Newsgroups: comp.programming
Path: sparky!uunet!destroyer!gatech!hubcap!mjs
From: [e-mail] (M. J. Saltzman)
Subject: Re: Help - What Is Wrong?
Message-ID: <[e-mail]>
Organization: Clemson University, Clemson SC
References: <[e-mail]> <[e-mail]> <[e-mail]>
Date: Wed, 11 Nov 1992 19:48:09 GMT
Lines: 145


In article <[e-mail]> [e-mail] (Markku Sakkinen) writes:
>In article <[e-mail]> [e-mail] (M. J. Saltzman) writes:
>>Discussing a fragment of code of the form
>>
>>    for ( i = 0;  i != 5;  i++ )
>>        ...
>>
>>[e-mail] (Richard M. Hartman) writes:
>>>
>>>I've always seen (and used) the "i<max" form of the for loop, and
>>>messed up when faced w/ anything else.  "i!=max" WILL work, but
>>>is less safe for a number of reasons (more so if initial condition
>>    ^^^^^^^^^
>>>is set by variable instead of literal).
>>
>>Presumably, "i != 5" is "less safe" because a failure of the initial
>>condition to satisfy i < 5 will not result in an infinite loop
>>(especially if the initializer "i = 0" is replaced by, say, "i = j + 1",
>>or if the initial i is passed as a parameter).  On the other hand,
>>this may not be the best kind of "safety" to have.
>>
>>In _The_Science_of_Programming_[1], David Gries argues that the guards
>>on loops should be as weak as possible, so that if the initial
>>condition is violated, the program will fail catastrophically (i.e.
>>with an infinite loop).  His reasoning is that the failure of i to be
>>less than 5 indicates an error elsewhere in the code, which might go
>>undetected if the loop fails to execute at all (with the program
>>giving a wrong answer).  If the program goes into an infinite loop,
>>you can be sure you've stumbled on a bug.
>
>Looks like pretty bad advice from such an acknowledged authority.
>If catastrophic failure is required, it should be an abort or the like,
>not an infinite loop.  Perhaps if the programmer herself is always
>tending to her programme when it is run(!), she may reason:
>"Far too much time has passed for this stage, it _must_ be stuck
>in an infinite loop somewhere."
>Infinite loops can be a particularly bad idea in multitasking systems.

But someone would catch such a loop pretty quickly, or you would run
out of resources (you do set time limits on your batch jobs, don't
you?).

I quote from the Master:

    Some object at first to finding the guard in this way, because
    Tradition would use the guard "i < n" instead of "i != n". However,
    "i != n" is better, because a software or hardware error that made
    i > n would result in nonterminating execution.  It is better to waste
    computer time than suffer the consequences of having an error go
    undetected, which would happen if the guard "i < n" were used.

I should also point out that this discussion is taken somewhat out of
context.  As someone pointed out in e-mail to me, the real reason for
weak loop guards is that the post-condition of the loop is a
conjunction involving the invariant and the negation of the guard.
Weak guards imply strong postconditions, which can help prove that the
loop accomplishes the desired function.  In fact, the guard is derived
as the complement of the postcondition needed to prove the desired
result.  Loop derivation also involves a bound function, bounded below
and decreased at every iteration, so termination is guaranteed if the
precondition is satisfied.

>In this specific example as is, there is not much difference
>between the alternatives.  But suppose a little modification:
>    for ( i = whiz(x);  i != 5;  i++ ) ...
>will be sensible only if you are absolutely sure that 'whiz(x)'
>returns a value < 5;  otherwise you should insert an explicit test.

That's right, and it is the point.  Remember that Gries's discussion
is in the context of deriving correct programs, so you have presumably
proved that the precondition "i < 5" is satisified in this case, but
if you should encounter a bug due to a typo, or someone else's code...

>On the contrary, 'i < 5' works perfectly also in this case,
>if the intent is not to execute the loop at all if the value is >= 5.

But if the intent is that i > 5 is an error, you want to write code
that will catch it.

>Also, the code might be modified so that the increment is 2 instead of 1;
>'i < 5' still works in a way that may be sensible.
>In general, it looks much more robust than 'i != 5'.

Surely if you are going to change the increment, you should re-derive the
guard as well!

>>On the other hand, Gries recommends that guards on "if" and "else"
>>statements should be as strong as possible, and that the default
>>action for any case not explicitly covered in the guards should be to
>>abort.  The reasoning is the same: if one of the "if" or "else"
>>conditions is not met, there is a failure elsewhere in the program
>>that could go undetected if the program is allowed to continue.
>
>Obviously you are quoting from memory (see below), and this does
>not make any sense.  'If ... then ... else ... endif'
>always covers all cases!

To be sure, it was from (recent) memory.  But let me elaborate:
Consider a piece of code that takes action based on the value of
some nonnegative variable k.  You might write:

    if ( k > 0 ) {
    ...
    } else {  /* k == 0 (since we're sure k >= 0) */
    ...
    }

Or you might write

    if ( k > 0 ) {
    ...
    } else if ( k == 0 ) {
    ...
    } else abort();

Gries's principle would advocate the latter, "all other things being equal."

>>[1] This book is a classic, and a very readable introduction to the
>>ideas underlying derivation of provably correct programs.  (Sorry, I
>>don't have the publisher information handy.)

Springer Verlag, 1981.

>If Gries strongly suggests infinite loops in many places,
>the book is evidently aiming at provably _partially_ correct programs. :-)

Oh, cheap shot!

>
>----------------------------------------------------------------------
>Markku Sakkinen ([e-mail])
>       [e-mail] (alternative network address)
>Department of Computer Science and Information Systems
>University of Jyvaskyla (a's with umlauts)
>PL 35
>SF-40351 Jyvaskyla (umlauts again)
>Finland
>----------------------------------------------------------------------


--
        Matthew Saltzman
        Clemson University Math Sciences
        [e-mail]