Nice. As usual, entry and exit conditions aren't that hard to write; it's loop invariants that are hard.<p><pre><code> /*@ loop_invariant
@ (\forall int i; 0<=i && i<stackSize-4;
@ runLen[i] > runLen[i+1] + runLen[i+2])
@ && runLen[stackSize-4] > runLen[stackSize-3])
@*/
</code></pre>
It's surprising how close their notation is to our Pascal-F verifier from 30 years ago.[1] Formal verification went away in the 1980s because of the dominance of C, where the language doesn't know how big anything is. There were also a lot of diversions into exotic logic systems (I used to refer to this as the "logic of the month club"). The Key system is back to plain old first-order predicate calculus, which is where program verification started in the 1970s.<p>For the invariant, you have to prove three theorems: 1) that the invariant is true the first time the loop is executed, given the entry conditions, 2) that the invariant is true for each iteration after the first if it was true on the previous iteration, and 3) that the exit condition is true given that the invariant is true on the last iteration. You also have to prove loop termination, which you do by showing that a nonnegative integer gets smaller on each iteration. (That, by the way, is how the halting problem is dealt with in practice.) #2 is usually the hardest, because it requires an inductive proof. The others can usually be handled by a simple prover. There's a complete decision procedure by Oppen and Nelson for theorems which contain only integer (really rational) addition, subtraction, multiplication by constants, inequalities, subscripts, and structures. For those, you're guaranteed a proof or a counterexample. But when you have an internal quantifier (the "forall int i") above, proof gets harder. Provers are better now, though.<p>A big practical problem with verification systems is that they usually require a lot of annotation.
Somebody has to write all those entry and exit conditions, and it's usually not the original programmer. A practical system has to automate as much of that as possible. In the example shown, someone had to tell the system that a function was "pure" (no side effects, no inputs other than the function arguments). That could be detected automatically. The tools have to make the process much, much easier. Most verification is done by people into theory, not shipping products.<p>[1] <a href="http://www.animats.com/papers/verifier/verifiermanual.pdf" rel="nofollow">http://www.animats.com/papers/verifier/verifiermanual.pdf</a>