Author: Vincent Diepeveen
Date: 17:07:42 02/28/03
Go up one level in this thread
On February 28, 2003 at 19:15:24, Gareth McCaughan wrote:
I know very well about the invariant Gareth. In fact i have a few books of the
guy who wrote about it in Dutch of course too.
A function is perfect if it has just an invariant because you have no extra
variables then. In this case that means for example getting rid of that loading
of the pointer.
this function you can strip the loop so far that you just keep left with the
invariant, which is a cool thing.
Best regards,
Vincent
>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.