Oh c*** - I'm talking to Andrew Koenig!?
Um, yes.
Thanks for discussing this though Andrew - I haven't had a discussion
that added spice to my blood in a couple of years!
You're quite welcome.
You still won't give an example of these "errors".
While my example is not only already provided - you can also have
something like this:
int N=3; # This is the index limit we have
int incr=2; # This is the loop incremental
int n=0; # This is the initial index
while (n != N) {
cout << f(n) << endl;
n+=incr;
}
Could crash when going to index 4 - which is out-of-bounds.. Or still
loop until n goes out of the integer limit.
Yes it could. However, this is something of an unusual example, as I think
you will see if you try to figure out the invariant of this loop.
It would be something like "we have called f(n) for values of n with the
following properties..." and because n is being incremented by a variable
(which, for all we know might change during the loop as a side effect of
calling f), those properties might be a bit of a pain to define exactly.
Right, from here I'll add some notes just to make sure I get the right
idea..
.. 0 <= n < N
Yes.
... and that intent is to step through each index (n) in the range:
0 <= n < N while:
0 <= n < i must also be held true
I prefer not to think of loops in terms of concepts such as "step through".
Instead, I like to think of them this way:
establish an invariant
while (a condition is true) {
change the values of variables while maintaining the truth of the
invariant
}
Then, after the loop terminates, I know that the invariant is still true,
and that the condition is now false.
In the example above, the invariant is
f(n) has been called for every integer n with 0 <= n < i
and the condition is i != N.
You mean i == N? (I take it as you do..)
Yes.
I think you are also missing a third statement from your proof.. That
you will call all values of i in the range:
0 <= i < N,
or increment i by the smallest integer value.
I don't understand this statement. I agree that it is necessary to prove
that we will call f(i) for all 0<= i < N, but that proof is a trivial
consequence of two claims:
1) The loop invariant is that we have called f(n) for all 0 <= n < i
2) After the loop terminates, i == N
The point is that the loop invariant is still true after the loop
terminates, so if i == N, we can substitute N for i in (1) above and see
immediately that we have called f(n) for all 0 <= n < N. If the loop
condition were i < N instead of i != N, we would still have to prove that i
> N was impossible.
Which can also be stated as:
You call f(n) for every value of n where 0 <= n < i while i != N
(conceivably allowing f(N) to be called if i goes above N)
Sorry -- when I said "we will call f(i) for all 0 <= i < N", I meant "for
all 0 <= i < N and no other values of i".
I take it again you meant i as an unknown value >= N .
Yes.
Which contradicts itself as the value of N may have possibly been passed
to f(n) - which it is unable to do.
Sorry; which *what* is unable to do?
This is better stated:
You call f(n) for every value of n where 0 <= n < i while i < N
I'll state this here;
In both cases, we assume that i is increased by the smallest integer
value, in which case the condition before invalidating the i < N
condition is where i = N-1 .
If you at all change the incrementing of the loop - or N - you can end
up in dangerous territory.
Indeed. But I think that's slightly off the point--at least the point I'm
trying to make.
The point I'm trying to make is that if your condition is i != N, you know
that after the loop terminates, i == N -- and you can use that fact in
reasoning about the program. If your condition is i < N, you know only that
i >= N, which is a weaker condition. So you have to go through additional
steps to show that even though i > N might be possible after the loop has
terminated, it cannot have happened while the loop was executing.
Again, I see no proof that either way can produce an incorrect answer.
If an 'incorrect' answer is produced, surely it is the code inside the
loop which would be at fault.
(I've put 'incorrect' as it is technically an 'undesired' or
'unexpected' result which is produced)
I completely agree that it is possible to prove that either form of the loop
is correct. I'm just saying that the proof is easier if the condition is i
!= N than if it is i < N.
I have no idea what you're talking about here.
Loading an input line (say from a file) into a data array (let's say
char[N}) while the length of the data is more than N.
(rather simplistic version)
If we're going to talk about pragmatics here, then we get into matters of
taste and experience. My experience is that it is common for people to
write i <= N when they really meant i < N, and that the problems that result
from such errors are exceedingly difficult to find. My taste is therefore
that it would be better to write i != N, yielding a program that works or
fails catastrophically, instead of possibly writing i <= N instead of i < N,
yielding a program that might fail undetectably.
But that's a matter of taste, about which reasonable people can disagree.
Also errors where a program is 'expecting' something to be correct.
When have humans ever been perfect, and 'correct' all the time? And why
should our programs expect this?
Programs don't expect anything; programmers do.
I try to program so that my code WILL do what I intend, but from the
above analysis - you are coming from the reverse angle - your code is
proven after the fact.
Proving code after the fact is extremely difficult, unless the code was
constructed in the first place to be easy to prove.
Thanks again for the discussion, it's really been an eye-opener.
You're quite welcome.
