Dafny Proofs From The Videos

If you try to follow the exact Dafny proofs from the lecture (or tutorial) videos you might find out that some may not work exactly. This is due to version change in Dafny from the time that the videos were prepared (Version 3) until now (Version 4). Bizarrely, the tool has been made stronger in some senses and weaker in the other senses. So, certain things that required manual hints before go through automatically now, and certain other proofs need help.

Note, also, that Dafny relies heavily on queries to a backend solver to check verification conditions and these queries are timed at a default. On different equipmenet, more or less time may be required for the same query to be successfully answered by the solver.

The principles you learn from these vidoes stand. The version changes in the tool do not change those.

GCD Correctness

For instance, the proof of correctness of gcd from the video is posted here. It requires a single (commented) change from the proof in the video to work at commandline.

In an editor (like VSCode), one sometimes observes nodeterministic behaviour from the backend solvers and gets different resutls. For instance, when nonlinear reasoning is required for one of the lemmas, it may require substantially more time. For instance, I use {:timeLimit 300} for the hardest lemma in the file above, because it takes quite some time on my old desktop to prove.

But, here is a proof with an additional lemma to help with nonlinear reasoning.

The above proof has a lot of redundancy that can be commented out. Things are intentionally spelled out so that you can see the entire proof. You can also further simplify the proof and lower its reliance on the solver. Do that as an exercise by yourself.

The rest

Program-type examples should mostly be ok. The majority of verison problems are related to arithmetic reasoning and the version change in the back end solver.