Dafny: reads clause

Sep 25, 2012 at 9:30 AM

I don't understand why Dafny doesn't use default strategy of choosing a decreases measure for function `p2' in this code: http://rise4fun.com/Dafny/bmf4  . Recursive invocation of `p2' occurs in `p2' itself so footprint of recursive invocation p2(x[1..]) must be the same as footprint of invocation p2(x) (and, so, I think, default strategy can work).

And the second question about the same program ( http://rise4fun.com/Dafny/bmf4 ). I understand function `p2' doesn't read "this". But how I should change body of `test2' to prove its postcondition with clause "reads this;" at `p2' ? 

(sorry for so many questions)

Coordinator
Sep 29, 2012 at 2:54 AM

Thanks for your questions.

The default strategy for choosing a decreases clause for a method is to take the lexicographic tuple of the method's in-parameter, leaving out those parameters that don't have a meaningful order.  So, an in-parameter whose type is a type parameter does not get included in the default decreases clause.

For functions, the situation is almost the same.  The difference is that if the function has a reads clause, then the default decreases clause is that reads set.  A better default order would be the lexicographic tuple starting with the reads clause, if any, followed by the parameters.  I implemented and checked in this change (available immediately in the sources and will be available on rise4fun with the next drop there).  In the meantime, either remove the "reads" clause from p2 (since it isn't needed) or add an explicit "decreases x;" clause.

(In the check-in, I also made a minor improvement in the error message produced.)

Your other question is more difficult.  You need a lemma.  The tricky thing (as you have probably noticed) is that the lemma needs to compare something in the "old" state and something in the present state.  Here is a way to do it:  http://rise4fun.com/Dafny/czjE

Program safely,
  Rustan

Coordinator
Sep 29, 2012 at 5:41 AM

In my previous post, I gave a rise4fun link to a program that answer the second question.  Call that program Program A.  Here's another version of the program, call it Program B:  http://rise4fun.com/Dafny/RpHH

In Program B, I'm using loops both before and after the assignment "x := [1] + x;" to inductively establish the property stated in the loop invariants.

In Program A, I used some fancy features that are good to know (but I think the loop in Program B is nicer here).  In Program A, I established the first inductive property in a separate lemma (the ghost method Lemma0).  The proof of Lemma0 (that is, the body of the ghost method Lemma0) calls Lemma1 for each "j".  Lemma1 is proved via a recursive call to Lemma1 (on a smaller "j").  If that recursive call were done explicitly, it would look like this:  http://rise4fun.com/Dafny/MZRb (Program C).  However, in Program B, I instead relied on Dafny's induction tactic (which, here, in effect calls Lemma1 recursively for *all* values smaller than "j").  The heuristic that turns on the induction tactic automatically does not kick in here (because "j" is not passed as a direct argument to the function p2, but sits inside the argument to p2 like y[j..]).  Therefore, I had to turn on the tactic manually, which I did using the {:induction j} attribute.

In summary, Program B uses Dafny's induction tactic but has to turn it on using an attribute.  Program C is thus simpler (in terms of what you need to know about Dafny's induction tactic), since it does an explicit recursive call to Lemma1.  Program A instead uses a loop, which makes the proof of the pre-"x := [1] + x;" property look more analogous to the post-"x := [1] + x;" property.  Note that the post-"x := [1] + x;" property cannot be proved by breaking it into a separate lemma, because the property needs to talk about two different heaps (which currently can only be done using the "old" construct).

  Rustan

Sep 29, 2012 at 10:00 AM

Oh, thank you very much, Rustan! So if I use "reads" or "modifies" clauses for methods and functions and invoke these methods and functions, I work with a lot of heaps (another word, I can think these functions have implicit input value (argument) - the heap - and implicit output value (returns) - another heap). I can change "implicit heap argument" to use "old" feature of Dafny. If I use many function invocations in one expression, I use these invocations with the same heap.

It is important that not all properties about one heap is carried out to another heap automatically. Instead of this I should use lemmas. But now I have a  recursive function. Dafny unrolls its invocation by 1 step and meets a property about "x[1..]" but before it works only with "x". So I should help Dafny to prove properties about "x[1..]" in basis of properties about "x". And to deal with this problem I should use induction. Induction starts with "assert old(p2([])) == p2([]);" which is obviously. The next steps are:

assert p2(y[k..]) == (|y[k..]| > 0 ==> y[k..][0] > 0 && p2(y[k..][1..]));//by def

assert y[k..][1..] == y[k+1..]; // by def of seq

assert old(p2(y[k+1..])) == p2(y[k+1..]); // by invariant

assert old(p2(y[k..])) == old(p2(y[k..][1..])) == old(p2(y[k+1..])) == p2(y[k+1..]);

assert p2(y[k..]) == p2(y[k..][1..]) == p2(y[k+1..]) == old(p2(y[k..]));

Thank you very much, Rustan ! I read your article about induction heuristic.