Author: Gareth McCaughan
Date: 16:15:24 02/28/03
Go up one level in this thread
On February 28, 2003 at 13:58:48, Vincent Diepeveen wrote:
> less instructions within the 'invariant' (i fear it might be a dutch word of a
> dutch professor who theoretically proved software and 'invariant' is describing
> all instructions which are getting executed within a loop) is excellent of
> course. Not doing the loading of the pointer within the invariant is trivially
> faster for most loops.
"invariant" is a perfectly good English word, and loops have invariants,
and there's at least one (recently deceased, alas) Dutch professor who
used them a lot. But they aren't anything like what you seem to mean here.
A loop invariant is a statement that is always true at a particular
point in the execution of a loop. They're very important when reasoning
about programs. So, for instance, in the following routine
int gcd(int a, int b) {
if (a<0) a=-a;
if (b<0) b=-b;
if (a<b) { int t=a; a=b; b=t; }
while (b>0) {
// . . . . . . . . . . . . . . . . . (1)
int t=a%b;
a=b; b=t;
}
return a;
}
you have the following loop invariant at (1), which you can prove
by induction:
a >= b > 0 AND
gcd(a,b) == gcd(a0,b0) where a0,b0 are the values of a,b on entry
which, combined with the "variant"
the value of b strictly decreases each time around the loop
proves that the returned value is the greatest common divisor
of the function's arguments.
It is absolutely not true that "'invariant' is describing all
instructions which are getting executed within a loop". The
invariant itself describes the state of the computer (and,
sometimes, its environment) at a particular point while a loop
is being executed. The word "invariant" describes the invariant :-).
The words "doing the loading of the pointer within the invariant"
don't make any sense. You may be looking for the term "loop body".
--
g
This page took 0 seconds to execute
Last modified: Thu, 15 Apr 21 08:11:13 -0700
Current Computer Chess Club Forums at Talkchess. This site by Sean Mintz.