We've now simplified the code of the "init" method substantially. Here's what my version looks like now:
method init(size: int)
modifies this;
requires size > 0;
ensures nextArray != null;
ensures forall j :: 0 <= j < nextArray.Length ==> -1 <= nextArray[j] < nextArray.Length;
ensures arrayInv();
{
elementArray := new int[size];
nextArray := new int[size];
parallel (j | 0 <= j < nextArray.Length) {
nextArray[j] := if j < nextArray.Length - 1 then j + 1 else -1;
}
usedHd := -1;
freeHd := 0;
usedSeq := [];
var fs, i := [], 0;
while (i < nextArray.Length)
invariant 0 <= i <= nextArray.Length;
invariant |fs| == i;
invariant forall j :: 0 <= j < i ==> fs[j] == j;
{
fs, i := fs + [i], i + 1;
}
freeSeq := fs;
}
What remains in the verification of this program is the hardest part--but as we'll soon see, once we figure out what the problem is (that is the hard part), the solution is simple.
The next problem is that the postcondition "ensures arrayInv()" does not verify. With different versions of the "init" method body, sometimes I get the postcondition violation reported, but sometimes I also received a time-out from the verifier.
The time-out is not so helpful, because it does not pin-point where the verifier was spending its time when time ran out. To debug a time-out, you currently have to temporarily comment out various things and see if that gets around the time-out. Often, but
not always, you'll find that the problem is something that Dafny has problems verifying. The verifier may then try extra hard to prove it, so hard that it gets totally bogged down and runs out of time.
Dafny reports a postcondition violation for "ensures arrayInv()", where "arrayInv()" is a user-defined predicate. Dafny also highlights, inside the body of "arrayInv()", which conjunct(s) it cannot prove. In this case, it points
us to the line:
(forall j :: 0 <= j < nextArray.Length ==> ((j in usedSeq) || (j in freeSeq))) &&
Perhaps this is a bug in our program, perhaps it indicates an error in the specification, or perhaps the error report comes from the verifier's inability to construct an appropriate proof. Here's how I would debug this problem.
First, copy the offending line to an assert statement at the end of the method body:
assert forall j :: 0 <= j < nextArray.Length ==> j in usedSeq || j in freeSeq;
What you should get now is a complaint about this assertion. But assuming that the asserted condition holds, we expect the postcondition to be verified. That is indeed the case here. So, what remains in our debugging is to figure out why we're getting a complaint
about this assertion.
Looking at the program, we expect that what the loop invariant says about "fs" should hold about "freeSeq" after the assignment "freeSeq := fs;". And knowing "freeSeq[j] == j" about each index j ought to mean that "j
in freeSeq" holds for each index, which in turn ought to imply the assert we added. To test this hypothesis, I would now write these things down. I'll write two new assert statements, so we end up with the following 3 assertions at the end of the "init()"
method body:
assert forall j :: 0 <= j < nextArray.Length ==> freeSeq[j] == j;
assert forall j :: 0 <= j < nextArray.Length ==> j in freeSeq;
assert forall j :: 0 <= j < nextArray.Length ==> j in usedSeq || j in freeSeq;
Dafny proves the first one, it complains about the second one, it proves the third one (which follows from the second assertion), and it proves the postcondition of the method (which follows from all the things that were proved automatically before, plus the
third assertion). So, what we have now discovered is that either our understanding of why the second assertion follows from the first is wrong, or Dafny is unable to prove that for us.
We're getting closer. Why can Dafny not prove the second assertion? To explore this further, it would be nice to "zoom in" on the proof argument for each j. We can do this with a "parallel" statement. We can replace the second assert with
something of the form:
parallel (j | 0 <= j < nextArray.Length)
ensures j in freeSeq;
{
// ...
}
(Alternatively, you can precede the second assertion with this parallel statement, to make sure you're stating the right thing. The second assertion gives the same condition that this parallel statement ensures, so we now expect to see a complaint about the
"ensures" clause of the parallel statement, but no other complaints.)
Let us now add to the body of the parallel statement what we believe to be true, namely:
assert freeSeq[j] == j;
Evidently, Dafny proves this assertion and is then able to prove the ensures clause of the parallel statement, which for all j's of the parallel statement implies the second assertion, which implies the third, which makes the whole method verify.
What I have just showed is a fairly typical way to go about debugging what's going wrong. You can closer by introducing assertions. And for this program, it was also useful to "zoom in" on the proof obligation by opening up a scope that allows us
to more easily speak about each "j".
What I'm about to say next is more advanced; ignore it if you don't care about the details. How come what we did helped Dafny construct the proof? I did not dive into the details to try to understand what Boogie programs/formulas were generated underneath Dafny's
covers or how the underlying SMT solver Z3 dealt with the formulas, but here's my hunch. The expression "j in freeSeq" gives rise to an existential quantifier, something like:
exists k :: 0 <= k < |freeSeq| && freeSeq[k] == j
Often when we deal with existential quantifiers, it is necessary to provide an explicit witness. In the process described above, we may have thought that the invariant freeSeq[j]==j would give that witness. It does, but this witness expression sits inside a
universal quantifier (which Z3 has to instantiate). The proof goal (here, the second assertion) is also a universal quantifier; since it's the proof goal, it will be negated and Skolemized, but the negation turns the "exists k..." into a universal
quantifier (which Z3 has to instantiate). Z3 then sits there with two contradictory universal quantifiers, but it doesn't know it because it doesn't know how to instantiate either of them. But providing the parallel statement, we get the opportunity to give
the witness closer to the existential quantifier, which does the trick. A different way to do this would be to not use the parallel statement and instead replace the second assertion with:
assert forall j :: 0 <= j < nextArray.Length ==> freeSeq[j] == j ==> j in freeSeq; // (*)
Here, too, we have placed the "freeSeq[j] == j" expression, which gives the witness, inside one level of universal quantification, thus getting closer to the existential entailed by the "in". But this assertion may not have been as easy
to invent, especially not if the formulas involved were more complicated than in this example.
In summary, now that we have figured out the extra information that Dafny needed to complete the proof, we can (if we so choose) delete the extraneous assertions that were needed only temporarily while we were debugging). You would then be left with, at the
end of the "init()" method, the parallel statement shown above. Or, instead of the parallel statement, you can give the assertion (*).