Communications of the ACM
Getting a Program Right (7)
(This article is part of a running series, which started here.)
In previous articles, I presented candidate binary search algorithms and asked whether they are correct. "Correct" means something quite precise: that for an array t and a value x, the final value of the variable Result is a valid index of t (that is to say, is between 1 and n, the size of t) if and only if x appears at that index in t.
In the previous article, I presented a new variant of the binary search algorithm -- relax, it was our last, you will not be asked to scrutinize any more version -- and boldly stated that it was correct. The question was: why?
In the case of the preceding versions, which were incorrect, you could prove that property, and I do mean prove, simply by exhibiting a single counter-example: a single t and x for which the program does not correctly set Result. Now that I asserting the program to be correct, one example, or a million examples, do not suffice. In fact they are almost irrelevant. Test as much as you like and get correct results every time, you cannot get rid of the gnawing fear that if you had just tested one more time after the millionth test you would have produced a failure. Since the set of possible tests is infinite there is no solution in sight [1].
We need a proof.
I am going to explain that proof in the next article, which will appear very soon [2], but before that I would like to give you an opportunity to look at the proof by yourself. I wrote in one of the earlier articles that most of what I have to say was already present in Jon Bentley's 1983 Programming Pearls contribution [3], but a dramatic change did occur in the four decades since: the appearance of automated proof system that can handle significant, realistic programs. One such system, AutoProof, was developed at the Chair of Software engineering at ETH Zurich [4] (key project members were Carlo Furia, Martin Nordio, Nadia Polikarpova and Julian Tschannen, with initial contributions by Bernd Schoeller) on the basis of the Boogie proof technology from Microsoft Research).
AutoProof is available for online use, and it turns out that one of the basic tutorial examples is binary search. You can go to the corresponding page and run the proof.
I am going to let you try this out (and, if you are curious, other online AutoProof examples as well) without too many explanations; those will come in the next article. Let me simply name the basic proof technique: loop invariant. A loop invariant is a property INV associated with a loop, such that:
- A. After the loop's initialization, INV will hold.
- B. One execution of the loop's body, if started with INV satisfied (and the loop's exit condition not satisfied, otherwise we wouldn't be executing the body!), satisfies INV again when it terminates.
This idea is of course the same as that of a proof by induction in mathematics: the initialization corresponds to the base step (proving that P (0) holds) and the body property to the induction step (proving that from P (n) follows P (n + 1). With a traditional induction proof we deduce that the property (P (n)) holds for all integers. For the loop, we deduce that when the loop finishes its execution:
- The invariant still holds, since executing the loop means executing the initialization once then the loop body zero or more times.
- And of course the exit condition also holds, since otherwise we would still be looping.
That is how we prove the correctness of a loop: the conjunction of the invariant and the exit condition must yield the property that we seek (in the example, the property, stated above of Result relative to t and x).
We also need to prove that the loop does terminate. This part involves another concept, the loop's variant, which I will explain next time.
For the moment I will not say anything more and let you look at the AutoProof example page (again, you will find it here), run the verification, and read the invariant and other formal elements in the code.
To "run the verification" just click the Verify button on the page. Let me emphasize (and emphasize again and again and again) that clicking Verify will not run the code. There is no execution engine in AutoProof, and the verification does not use any test cases. It solely processes the text of the program as it appears on the page and below. It applies mathematical techniques to perform the proof; the core property to be proved is that the proposed loop invariant is indeed invariant (i.e. satisfies properties A and B above).
The program being proved on the AutoProof example page is version #6 from the last article, with different variable names. So far for brevity I have used short names such as i, j and m but the program on the AutoProof site applies good naming practices with variables called low, up, middle and the like. So here is that version again, but with the new variable names:
-- Program attempt #7 (identical to #6 with different variable names) .
from
low := 1 ; up := n + 1
until low ≥ up or Result > 0 loop
middle := low + ((up - low) // 2)
if a [middle] < value then -- The array is now called a rather than t
low := middle + 1
elseif a [middle] > value then
up := middle
else
Result := middle
end
end
This is exactly the algorithm text on the AutoProof page, the one that you are invited to let AutoProof verify for you. I wrote "algorithm text" rather than "program text" because the actual program text (in Eiffel) includes the variant and invariant clauses that do not affect the program's execution but make the proof possible.
Whether or not these concepts (invariant, variant, program proof) are completely new to you, do try the prover and take a look at the proof-supporting clauses. In the next article I will remove any remaining mystery.
Post-publication note: the announced "next article" appears here. Carried over the copy-paste error fix for versions #5 and #6.
Note and references
[1] Technically the set of possible [array, value] pairs is finite, but of a size defying human abilities. As I pointed out in the first article, the "model checking" and "abstract interpretation" verification techniques actually attempt to perform an exhaustive test anyway, after drastically reducing the size of the search space. That will be for some other article.
[2] I hope tomorrow, circumstances permitting.
[3] Jon Bentley: Programming Pearls: Writing Correct Programs, in Communications of the ACM, vol. 26, no. 12, pp. 1040-1045, December 1983, available for example here.
[4] The AutoProof page contains documentations and numerous article references.
Bertrand Meyer is chief technology officer of Eiffel Software (Goleta, CA), professor and provost at the Schaffhausen Institute of Technology (Switzerland), and head of the software engineering lab at Innopolis University (Russia).
Comments
Berend Ottervanger
I know this article is old, but since I got here through your more recent article on AI not being as good for programmers as everyone thinks, it might still be interesting to know that program attempt 7/6 are both incorrect. They are different from the automatic prover implementation. low/i := 0 instead of 1 and up/j := n instead of n + 1. Making the invariant not hold initially. That is, a/t := [0, 1], x := 1 will fail, returning 0, or even a/t := [0], x := 0 failing because the array is indexed at 0, which doesn't exist.
Displaying 1 comment