I'm working through Leino's nice book "Program proofs" ((c) date 2023). The book is really well-written, explains thoroughly and progresses exactly as I need. But as I'm reproducing examples and solving exercises, I'm disappointed with some of the exercises: In VSC with Dafny 4.10.0, some (e.g. exercises 3.0, 3.1, 3.4) verify automatically, leaving nothing to exercise :-)
As another example, the simple algebraic equations on page 107 that are supposed to motivate proof calculations all verify without any manual contribution whatsoever. The same is true for the corresponding exercises on page 108 (5.4 a-c):
lemma {:induction false} ex_5_4_a(x: int, y: int)
ensures 5*x - 3*(y+x) == 2*x-3*y
{}
lemma {:induction false} ex_5_4_b(x: int, y: int)
ensures 2*(x+4*y+7) -10 == 2*x+8*y+4
{}
lemma {:induction false} ex_5_4_c(x: int, y: int)
ensures 7*x+5 < (x+3)*(x+4)
{}
I am using {:induction false} where suggested in the book, and that does help where induction is needed, but (unsurprisingly) not in these cases.
In my understanding, using {:only} or {:verify false} wouldn't help because I do want verification -- but "less automatically".
I'm aware that verification sometimes doesn't start at all when the file contains syntax errors, so incorrect code gets (or retains) the green check mark anyway. But my file doesn't seem to have any errors.
The book's web page https://www.program-proofs.com/ doesn't mention the effect.
Has the Dafny engine grown more powerful since the book was written, rendering some exercises obsolete? Can anybody explain the effect, and maybe recommend a workaround?
Thank you for the book praise. I'm delighted to hear it explains what you want to learn.
You're right that Dafny does prove those exercises automatically from the given program text. (I believe this behavior is the same in Dafny 4.10 as it was in Dafny 4.0 at the time the book was published.) Dafny's behavior (as explained later, in section 3.4 of the book) is that if you don't provide any decreases clause, then Dafny provides a default decreases clause. In these exercises, the default decreases clause provides what the verifier needs to prove termination.
The exercise asks you to write an explicit decreases clause. If you do that, then you will not get the default decreases clause, and thus you have to provide the answer yourself. That is, think of Exercise 3.0 as asking you to replace the ... in
function F(x: int): int
decreases ...
{
if x < 10 then x else F(x - 1)
}
with something that makes the function verify, without deleting the decreases clause or otherwise changing the function definition.
I agree that it would be fair if the book pointed this out. That is, it would be good if at least this first exercise said more forcefully that you have to write your own decreases clause and to point out that Dafny has certain defaults (explained in Section 3.4) that make it able to verify termination in the absence of any decreases clause.
True, again. Dafny can prove those arithmetic properties without a detailed calc statement. In section 5.4, my goal was to introduce and explain the calc statement. But, as you point out, Exercise 5.4 is too easy, because you don't actually need a proof calculation at all. (Turning off automatic induction doesn't change anything here, because the equations in the exercise are proved directly, without the use of induction.)
To practice writing less trivial proof calculations, see the remaining subsections of Chapter 5---and for that matter, the rest of the book. Probably the best chapter to get practice with writing proofs and calc statements is Chapter 6. The material there is still simple, so you can learn the form of the proofs rather than needing to come up with clever insights that make the proofs go through.
Thanks,
Rustan