Dafny Resources and Tutorials

This page has been prepared as a guide for Dafny.

• Official Website: follow the links there for installation, reference manual, etc.

Note: The videos for the lectures and tutorials were prepared using an older version of the plugin for Dafny in VSCode. The one you download and use today may look slightly different. The principles should remain the same.

Video Tutorials

• Preconditions and Postconditions: how to define preconditions and postconditions for methods via requires and ensures.

• Assertions: verifying that a property holds at a given program location using assert statements.

• Loops and Invariants: using invariant clauses to specify loop invariants. Using decreases clauses to specify termination measures.

• Arrays: how to reason about arrays. Using quantifiers and old expressions. The purpose of the modifies clause.

• Recursion: reasoning about recursion using binary search as an example.

• Sequences: reasoning about sequences using merge sort as an example.

• calc: using the calc construct to prove chains of equivalences.

• Functions: writing functions and proving properties involving them.

Dafny Arguments

The following code forces Dafny to spend no more than one second verifying individual verification conditions. This is helpful if you want to keep your proofs simple and quick to verify. It should be pasted in your settings .json in Visual Studio Code.

"dafny.serverVerifyArguments": [
        "/timeLimit:1"
]