Dafny: function termination

Sep 21, 2012 at 11:43 AM

I'm wonder why Dafny can't prove "termination" for `count2' but doesn't have any problem with `count3' : http://rise4fun.com/Dafny/p4mK .

Sep 21, 2012 at 11:47 AM

And the same question about datatypes: http://rise4fun.com/Dafny/vHz0 .

Coordinator
Sep 21, 2012 at 6:51 PM

The problem in the two non-verifying examples is that the postcondition mentions a recursive call, but the recursive call has "larger" parameters than the function itself.

Perhaps it helps to think about what would happen if, hypothetically, the specifications were evaluated at run time.  In that case, after a call to count2(s,x), it would be time to check that its results lives up to the postcondition.  This check involves checking the equality count2(s+[x], x) == count2(s, x).  The right-hand side has just been computed (because it denotes the function itself), but now it also needs the value of count2(s+[x], x), so the run-time system would invoke count2 again.  At the end of evaluating count2(s+[x], x), its postcondition would be checked, which involves the equality count2(s+[x]+[x], x) == count2(s+[x], x).  This requires another call to count2, and so on.  So this process would not terminate.

In the previous paragraph, I described the checking of the postcondition as if it were done at run time.  But essentially the same thing goes on during verification.  (Perhaps it is possible to argue, somehow, that this infinite recursion is unproblematic since it only occurs in a postcondition.  I thought about it for a few minutes and I couldn't think of an example where that would make the verification unsound.  But checking those recursive calls for termination, like Dafny currently does, is sound.)

In count3, the recurisve invocation count3(s[1..], x) does decrease something, namely the length of the first argument (which is what the "decreases" clause says decreases), so this recursion does not go on forever.  I would recommend trying to formulate your postconditions that way.

One more thing, if you do want to prove a property that involves several invocations of a function, you can do that as a lemma (see http://rise4fun.com/Dafny/WQ6H and below).  To make use of the lemma, you would then have to invoke the Lemma_about_count2 method.

function count2(s : seq, x : int) : nat
  decreases |s|;
  ensures count2([], x) == 0;
  ensures |s| < |s + [x]|;
  // The following two properties are proved in the lemma below:
  // ensures count2(s + [x], x) == count2(s, x) + 1;
  // ensures forall y :: y != x ==> count2(s + [y], x) == count2(s, x);  

ghost method Lemma_about_count2(s : seq, x : int)
  ensures count2(s + [x], x) == count2(s, x) + 1;
  ensures forall y :: y != x ==> count2(s + [y], x) == count2(s, x);  
 


  Rustan

Sep 22, 2012 at 8:48 AM

Ok, thank you! I'm looking for a way to use Dafny for dealing with algebraic specifications (and axiomatic specifications also). And now I understood I should use ghost methods without bodies for axioms and ghost methods with bodies for lemmas.