CSC410 Dafny Resources

• Official Documentation
• Quick Reference
• Reference Manual

Video Tutorials

1. Preconditions and Postconditions

   How to define preconditions and postconditions for methods via requires and ensures.

2. Assertions

   Verifying that a property holds at a given program location using assert statements.

3. Loops and Invariants

   Using invariant clauses to specify loop invariants. Using decreases clauses to specify termination measures.

4. Arrays

   How to reason about arrays. Using quantifiers and old expressions. The purpose of the modifies clause.

5. Recursion

   Reasoning about recursion using binary search as an example.

6. Sequences

   Reasoning about sequences using merge sort as an example.

7. calc

   Using the calc construct to prove chains of equivalences.

8. 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"
    ],