From: sakkinen@jyu.fi (Markku Sakkinen)
Subject: Re: Help - What Is Wrong?
Organization: University of Jyvaskyla, Finland
Date: Fri, 13 Nov 1992 10:31:53 GMT

In article <1992Nov11.194809.18616@hubcap.clemson.edu> mjs@hubcap.clemson.edu (M. J. Saltzman) writes:
>
>In article <1992Nov10.135848.3730@jyu.fi> sakkinen@jyu.fi (Markku Sakkinen) writes:
>>In article <1992Nov9.154402.16285@hubcap.clemson.edu> mjs@hubcap.clemson.edu (M. J. Saltzman) writes:
>>>Discussing a fragment of code of the form 
>>>
>>>	for ( i = 0;  i != 5;  i++ )
>>>		...

[A lot of discussion deleted.]

>>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?).

There are no time limits for background processes in vanilla UNIX systems,
for instance.  A task caught in an infinite loop may go undetected for
a long time, slowing down the whole system.  (I speak from experience.)

>I quote from the Master:

I never knew these things were treated already in the Gospels :-)

>	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.

(We'll keep in mind that this quote pertains to a more general situation.)
In the specific example from which this discussion sprung up (still
conserved above!), it is simply ludicrous to fear for 'i > 5'
immediately after setting 'i' to 0!  Or, if the hardware or system software
is as bad as that, there is not much idea to discuss the correctness
of one's own code.

>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

I don't think that it necessarily matters.
There is a neat little case, on which everybody can try to convince
others about the virtues of his/her favourite principles or theory.

> ...
>>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...

I don't understand.  If I don't know about 'whiz' with certainty,
but am interested in getting a correct programme,
why should I be lazy and let the loop run infinitely, instead of
putting an assertion about 'i <= 5' in the first place?

>>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!

It seems a bit as if you (and the book?) were taking a pure top-down
approach:  if the specification changes, you forget the old code and
derive the whole thing again beginning from the specification.
If one is modifying software more incrementally, considerations
like this matter a lot.  (In fairness, such modifications to the example
could be imagined in which 'i != 5' would remain correct but 'i < 5'
would need modification.)

>>>On the other hand, Gries recommends that guards on "if" and "else"
>>> ...
>>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:
> ...
>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."

All right, this clarifies the point.
But see the posting by Vadim Antonov that has come in the meantime.

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

I don't think so.  After all, 'partially correct' means that the programme
fulfills its specification _if_ it terminates, 'totally correct' meaning
that also the termination is assured.  I could have said that
  loop null end loop
is a partially correct programme with respect to any specification,
so we can go on to attend to some other business.  Now, _that_
would have been a cheap shot.

----------------------------------------------------------------------
Markku Sakkinen (sakkinen@jytko.jyu.fi)
       SAKKINEN@FINJYU.bitnet (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
----------------------------------------------------------------------
Newsgroups: comp.programming