
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)



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 inparameter, leaving out those parameters that don't have a meaningful order. So, an inparameter 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 checkin, 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



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



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.

