Loop Invariants

a > b is the same as b < a and I would argue a > b is clearer in this instance by noting the symmetry of the following line:

    if ( a[smallestSoFar] > a[nextToCheck] ) {
      smallestSoFar = nextToCheck ;
    }

When a > b then a = b

The order of the variables doesn't change.

The value is called nextToCheck because the article is specifically talking about loop invariants. The value of nextToCheck only makes sense when loop invariant is established prior to the loop and after work has been done in the loop to reestablish the loop invariant.

In both of those cases the value in nextToCheck is clearly meant to denote the half open interval [0, nextToCheck) which contains the smallestSoFar.

currentComparisonIndex is not the correct name for the loop variable because that name is only accurate after checking the termination condition and prior to incrementing. This is not what the loop invariant states the purpose of nextToCheck is. Therefore you would not have established a proper loop invariant prior to entering your loop. nextToCheck might more fully be called 'nextToCheckAfterTerminationCheck'

Of course this is all meta above the level of the language is self. You could call the variable 'foo' and of course the code would still function.

The halting problem is just an example. The real concern is that any "nontrivial" program property is also undecidable (see Rice's Theorem)

That's a good point. But then, tail-recursive functions are loops, so I guess I should have expected the correspondence.

Of course it's proof by induction. You prove that it's true for iteration N+1 if it was true for iteration N. You prove that it was true for iteration 0. Then you're done.

Here's how we did it in the Pascal-F verifier [1] around 1980. This is the simplest example - proving that all entries in an array are zero after the array is initialized.

    type tabix = 1..100;
    type tab = array [tabix] of integer;
    rule function allzero(a: tab; i,j: tabix): boolean; begin end;
    var table1: tab;
       i,j: tabix;
    ...
    for i := 1 to 100 do begin
        table1[i] := 0;
        assert(allzero(table1,1,i-1));
        state(allzero(table1,1,i));
    end;
    assert(allzero(a,1,100));
    ...
    assert(table1[j] = 0);   { table1[j] must be 0 }

The loop invariant is

    state(allzero(table1,1,i));

which says that the predicate "allzero" is true for table1 from 1 to i.

"allzero" is defined in the Boyer-Moore theorem prover as a recursive function.

    (defn allzero (a i j) 
        (if (lessp j i) 
            t 
            (and (allzero a (add1 i) j) (equal (selecta! a i) 0))))

That's a recursive function. The prover is able to prove that it terminates. "(selecta! a i)" is LISP for "a[i]" here.

We need three theorems about "allzero". First, that it's vacuously true for j < i:

    (implies (and (arrayp! a)
                  (numberp i)
                  (numberp j)
                  (lessp j i))
             (allzero a i j)))

Notation: "arrayp!" is true if the item is an array. "numberp" is true if it's an integer. "lessp" is "<".

Then that it's true for a single element if that element is zero:

    (implies (and (arrayp! a)
                  (numberp i)
                  (numberp j)
                  (equal i j)
                  (equal (selecta! a i) 0))
             (allzero a i j))))

And finally, the hard one, that if it's true up to N, and a[N+1] is zero, it's true up to N+1.

    (implies (and (arrayp! a)
                  (numberp i)
                  (numberp j)
                  (allzero a i j)
                  (equal (selecta! a (add1 j)) 0))
             (allzero a i (add1 j))))

These are all proved, once, with the Boyer-Moore theorem prover. Once proven, they can be used as rules by the much simpler and faster Oppen-Nelson prover built into the Pascal-F verifier. Over time, you build up a library of such rules, which are applied automatically by the fast prover.

This is 1980 technology; there's been a lot of progress in the last 35 years. This ran on a 1 MIPS VAX 11/780 and later on Sun II workstations. Back then, it was very slow to do this. That's a solved problem. It's still rather painful. But it works.

[1] http://www.animats.com/papers/verifier/verifiermanual.pdf

You can view it as induction, although the general case is slightly different. In the general case you have a while loop with some condition and invariant, and after the while loop stops your invariant is true and the condition is false, if you've done things correctly this then implies your 'goal'.

So to find a minimum in a list A[1],A[2],...,A[n] you can something like:

    i := 1;
    // Invariant: A[min] is the smallest in {A[1], ..., A[i]}
    while not i = n do begin
        if A[i+1] < A[min] then min:= i+1;
        i:= i+1;
    end

The negation of the condition: 'i = n', combined with the invariant: 'A[min] is the minimum of {A[1], ..., A[i]}', gives you the result you wanted.

Here's binary search from Go's sort package:

    func Search(n int, f func(int) bool) int {
        // Define f(-1) == false and f(n) == true.
        // Invariant: f(i-1) == false, f(j) == true.
        i, j := 0, n
        for i < j {
            h := i + (j-i)/2 // avoid overflow when computing h
            // i ≤ h < j
            if !f(h) {
                i = h + 1 // preserves f(i-1) == false
            } else {
                j = h // preserves f(j) == true
            }
        }
        // i == j, f(i-1) == false, and f(j) (= f(i)) == true  =>  answer is i.
        return i
    }

There's lots more examples of you search for "invariant" thru the std library source code.

A few, to give a taste:

ast/print.go printer.Write

    // invariant: data[0:n] has been written

printer/printer.go trimmer.Write:

    // invariants:
    // p.state == inSpace:
    //  p.space is unwritten
    // p.state == inEscape, inText:
    //  data[m:n] is unwritten

path/filepath/path.go: path.Clean

    // Invariants:
    //  reading from path; r is index of next byte to process.
    //  writing to buf; w is index of next byte to write.
    //  dotdot is index in buf where .. must stop, either because
    //      it is the leading slash or it is a leading ../../.. prefix.

Invariants really are a really useful way to think about code.

Here's an example in a getline implementation: https://github.com/eliteraspberries/ttyprompt/blob/master/ge...

        /*@ loop invariant i;
            loop invariant j >= 0;
            loop assigns j, eol;
         */
        for (j = 0; j < (size_t) i; j++) {
            if (read_buffer[j] == '\n') {
                eol = 1;
                j++;
                break;
            }
        }

Loop invariants are part of the ACSL specification language, and they can be verified automatically with Frama-C. http://frama-c.com/acsl.html

Weirdly, I hadn't tripped over 'loop invariant' in years, then I scribbled my own ode to them[1] and now this.

Loop invariants get important in the section on Bentley-McIlroy three section partioning.

[1] http://maniagnosis.crsr.net/2016/02/quicksort.html

I wrote a Babel plugin which brings a similar syntax to JavaScript, so you can write this:

    for (let i = 0; i < someVar; i++) {
       invariant: i < 10000; 
       console.log(i);
    }

along with other kinds of contract, like preconditions and postconditions - https://github.com/codemix/babel-plugin-contracts

This kind of proofs usually are separated in two steps:

- correction: define a loop invariant. Assuming the loop terminates, it will hold when the program exits the loop.

- termination: define a loop variant, something that changes at every iteration. If you can find a variant that is a strictly decreasing sequence of natural numbers (or an increasing, bounded sequence), you've established that the loop terminates.

Once you've done these two steps you know that the program terminates and the invariant holds at the end. (in your case, you won't be able to find a good variant - depending on the floating point semantics you use of course).

The two loop invariants would be: 1.0 == total + delta * 2 and delta > 0, so the while condition would never be false.

The amount of memory required to store the delta variable should be at least log_2(n) bits, where n is the iteration number. This has to be true, regardless of the implementation details of bigFloat because delta has to take on n distinct values. Eventually it exhausts the memory of the machine.

It seems pretty straightforward, unless your compiler is smart enough to see what's going on and optimize the body of the loop away, in which case it wouldn't terminate.

You're asking for a loop invariant to prove that a non-terminating loop terminates? That seems... somewhat contradictory. Either you can't prove that with a loop invariant, or the proof must be invalid.

As you said, the machine eventually runs out of memory. But "loop invariants" don't usually include the machine running out of memory as the termination condition, because that's more a crash than a loop termination. (That is, whatever part of the program you wanted to execute after the zeno loop won't execute, because the program terminated, not just the loop.) So when we talk about loop termination, program-crashing events are usually out of scope. (That's something we also need to prove - no undesirable side effects - but that's actually a separate issue.)

delta > epsilon

when this is false, the loop should terminate

even BigFloats have limited precision

Termination is not about the loop invariant. You also need a measure of termination, which is usually a nonnegative integer which decreases on each iteration.

In our Pascal-F system, we had a MEASURE statement for that. You didn't need it for FOR loops, though.