"Simple" program won't verify

Feb 18, 2013 at 10:16 AM
Hi Rustan,

Could you give me some advice on how to formulate this so that it will verify? I have tried various ways of structuring the quantifiers (together, nested etc.), but in all cases it either says the assertion fails, or it loops.

The program's below.

Thanks!

function isSubsequence (bs: seq<int>, cs: seq<int>): bool
{ if (cs==[]) then
    true
else if (bs==[]) then
    false
else if (bs[0]!=cs[0]) then
    isSubsequence(bs[1..],cs)
else isSubsequence(bs[1..],cs[1..])
}

method Test() {
assert
forall bs,cs::
    isSubsequence(bs,cs)
    ==>
    forall b:: isSubsequence(bs+[b],cs)
;
}
Coordinator
Feb 19, 2013 at 1:56 AM
(As you have noticed) Dafny does not prove this property automatically. You have to help it along. In the following program, I'm using three useful tricks, which solve the problem (that is, they lead Dafny to the desired proof). You may be able to combine or shorten the steps I'm showing here, but let me explain things in the order I did them, which may prove instructive--doing steps like this may also help keep your sanity and lower frustration (but, as always... your mileage may vary).

First, to prove the universally quantified condition in the assert, we can consider a particular bs,cs,b triple and prove the property for it. The easiest way to do that is to write a lemma (as a ghost method), parameterized by bs,cs,b, and then to invoke this lemma for all values of bs,cs,b. So, declare the lemmas as:
ghost method TestOne(bs: seq<int>, cs: seq<int>, b: int)
  requires isSubsequence(bs,cs);
  ensures isSubsequence(bs+[b],cs);
and precede the assert with the following statement:
  parallel (bs, cs, b | isSubsequence(bs,cs)) {
    TestOne(bs, cs, b);
  }
which performs an infinite number of calls to TestOne, reaping the postcondition of each one. In fact, the postcondition of the parallel statement will be exactly the condition given in the assert.

Next, we need to provide a body for the TestOne method, that is, we need to provide a proof for the TestOne lemma. If cs or bs is the empty sequence, the lemma follows directly from the definition of isSubsequence, so we start by writing:
  if (cs != [] && bs != []) {
    // to be filled in
  }
We are now about to apply the second trick, which is a proof calculation. (I know you are familiar with them on paper, and you can also do them in Dafny.) To make our formulas simpler, let's give names to two expressions:
    var bb, csx := bs + [b], if bs[0] != cs[0] then cs else cs[1..];
To do the calculation, just start writing out the proof you would write by hand. With each step, you can see if Dafny can follow--this is a great way to debug what it is that Dafny understands and where it gets stuck. Here's the full calculation:
    calc {
      isSubsequence(bs, cs);
    ==  // def. isSubsequence
      isSubsequence(bs[1..], csx);
    ==> { TestOne(bs[1..], csx, b); }
      isSubsequence(bs[1..] + [b], csx);
    ==  { assert bs[1..] + [b] == (bs + [b])[1..]; }
      isSubsequence(bb[1..], csx);
    ==  // def. isSubsequence
      isSubsequence(bb, cs);
    }
A thing to note: The first and last steps of this calculation make use of the definition of isSubsequence. Since Dafny knows how to do this, you don't need to supply any hint to Dafny. However, for your own documentation purposes, you can add a comment, just like I have done here.

Another thing to note: The second step is a weakening, as indicated by using the implication operator. The justification of this proof step comes from invoking TestOne recursively. In other words, it is making use of the "induction hypothesis" of our proof goal. Dafny will, of course, check that you're calling TestOne on "smaller" input, which ensures that the recursion is well-founded. As it turns out, because of Dafny's automatic induction tactic, you don't need to supply a hint here, but you can if you like.

The remaining hint contains the third trick. Or, workaround, if you wish. While Dafny usually handles sets with ease, it chokes up on some properties of sequences. What we need here is a distribution property of the "drop" operator and concatenation. By stating that property as an assertion, Dafny will try to prove the asserted condition (which it can do--but it wouldn't have thought of that this would be a good condition to prove) and will then assume it. Thus, an appropriate hint for this step in the calculation in an assert statement. If you were debugging this yourself, you may have written the calculation step, then received a complaint from Dafny, and then tried harder (as I did) to justify the step by providing a further hint in the calculation step.

Note: The syntax of the "calc" statement changed earlier this week. I'm here showing the new, nicer format. If you build Dafny from the latest sources, this is what Dafny expects. Rise4fun is not yet updated, so if you want to run this program on rise4fun today, use this program.

So, the "calc" statement not only lets you debug a verification attempt, but it can also give you a readable proof afterwards. Dafny won't insist on having the readable proof, as long as you provide it with the crucial ingredients of the proof. In this case, the crucial ingredient that Dafny didn't figure out itself was the property about sequences. So, you could have replaced the entire body of TestOne with just:
  assert bs != [] ==> bs[1..] + [b] == (bs + [b])[1..];
Rustan