Bugs in Dafny tutorial

[johnwickerson]

I found a few bugs (and other opportunities for mild improvements) in the Dafny tutorial that I thought it might be useful to report.

• "If statements require parentheses around the boolean condition" -> should say "do not require".

• In the spec for Abs, you have ensures 0 <= x ==> x == y and ensures x < 0 ==> y == -x. These could be made more symmetric if the first clause said ensures 0 <= x ==> y == x"

• "What precondition doe you need" -> typo

• "Dafny will complain that our post condition doesn't hold" -> should be "postcondition"

• "repairing it relatively easy" -> missing "is"

• "But the crucial step from the loop to the postcondition wouldn't hold." -- I don't think this sentence is true. I think that the reasoning itself still holds, it's just that it doesn't tell us that the loop terminates.

[RustanLeino]

Nice suggestions. Thank you!

Once the PR gets approved and merged, the changes will go out on rise4fun with the next release there (which will probably coincides with the next binary release of Dafny).

[jtojnar]

It has been over a year, more than two years for some of the older fixes. Is the rise4fun update still planned?