Hacker News Reader

Comment by tmerr | Hacker News Reader

Hey, this seems like an application of induction. You choose some property you want to prove about your program, show it is true before the loop (base case), then show it remains true for any next iteration (inductive step), therefore it is true for all iterations.

It reminds me of the hand-wavy inductive proofs I run through my head when I write recursive functions. Usually it's not even about eliminating bugs, it's just the most natural way to understand why the code works. It seems less natural for imperative for/while loops but still a good tool to keep in mind.

View on HN

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.

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

Reply on news.ycombinator.com