Prerequisites

Programming experience in C-style languages—Java, C, C#, JavaScript, etc.—must be assumed. The Dafny language reference and the Dafny Guide will be extremely useful resources for you. Finally, there’s a quick reference and cheat sheet if you need a refresher.

Note

Code snippets can be copied by hovering over the snippet and clicking the button which appears on the top right.

Some snippets are declared as files—those can be downloaded directly by clicking the button next to the filename.

Instructions

If you’re using the computers in the lab, everything should already be installed—just open VS Code.

If you’re using your own computer, install VS Code, run it, hit Ctrl+Shift+X / ⌘⇧X to bring up the extensions menu, then search for and install the Dafny extension.

In either case, create the following file:

Test.dfy
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
method Abs(n: int) returns (result: int)
    ensures result >= 0
    ensures result == n || result == -n
{
    if n < 0 {
        result := -n;
    } else {
        result := n;
    }
}

method {:main} TestAbs()
{
    var x := Abs(-3);
    assert x == 3;
    print x, "\n";
}

All going well, you should see a message at the bottom-left which reads ‘Verification Succeeded’. If so, the installation was successful. If not, try reloading the window (Ctrl+Shift+P / ⌘⇧P, then type ‘Reload Window’ and press Enter). Press F5 to compile and run the code.

Dafny’s verifier can sometimes get stuck trying to verify correct code. If you think Dafny should be verifying what you’ve written, try reloading the window. If it still doesn’t work, then there’s a real problem you must address.

If you’re already comfortable with Dafny, you can skip right ahead to the lab questions. If you are not, then I strongly recommend reading the next few sections carefully, since they will help prepare you for the lab.

General Tips

  1. Dafny accepting your code as verified is not by itself an indication that you have answered the question correctly.
  2. You may know your code is correct before Dafny does. The goal is not to write correct code, but to write code that Dafny can verify to be correct. Correct code is therefore not by itself an indication that you have answered the question correctly.
  3. Correct code and a verified postcondition together are not an indication that you have answered the question correctly.
  4. A weak condition is satisfied by many models. A strong condition is satisfied by few models.
  5. Always look for the weakest precondition. The ideal precondition is no condition at all. Ask for what you need, and no more.
  6. Always look for the strongest postcondition. A postcondition is strengthened by exposing its weaknesses. Try to imagine output which satisfies your postcondition, but behaves in a way that you do not want or expect. What your code really does is irrelevant here—it may well be correct. But the postcondition is the means by which you communicate what your code does to the rest of the program. If it is too weak, then other methods may not know enough about what your code guarantees to progress with their own proofs.

Worked Example

To illustrate points 3–6, consider the following code which computes the absolute value of any \(x \in \Z\), denoted mathematically as \(\lvert x \rvert\).

1
2
3
4
5
6
7
8
method Abs(x: int) returns (result: int)
{
    if x < 0 {
        result := -x;
    } else {
        result := x;
    }
}

The code is correct, but it has no contract. This prevents the verifier from inferring anything about the code. For example, even this simple assertion will fail.

1
2
3
4
5
method {:main} TestAbs()
{
    var x := Abs(-3);
    assert x >= 0;  // ✗ fails
}

Let’s fix that by adding a silly contract.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
method Abs(x: int) returns (result: int)
    requires -10 < x < 10
    ensures result >= 0  // ✓ succeeds
{
    if x < 0 {
        result := -x;
    } else {
        result := x;
    }
}

Dafny can prove both the postcondition and the assertion automatically.

1
2
3
4
5
method {:main} TestAbs()
{
    var x := Abs(-3);
    assert x >= 0;  // ✓ succeeds
}

In some sense, this code is ‘correct’—but it has some issues. The precondition requires that \(-10 < x < 10\), but the absolute value function should work for any integer, not just a small range of them. If we use any integer outside this range, Dafny will complain that the precondition is violated.

1
2
3
4
5
method {:main} TestAbs()
{
    var x := Abs(-10);  // ✗ fails (precondition violation)
    assert x >= 0;
}

Since there is no good reason to restrict Abs in this way, we can remove it. Of course, the postcondition still holds.

1
2
3
4
5
6
7
8
9
method Abs(x: int) returns (result: int)
    ensures result >= 0  // ✓ succeeds
{
    if x < 0 {
        result := -x;
    } else {
        result := x;
    }
}

Let’s see what Dafny can infer about the function now.

1
2
3
4
5
6
method {:main} TestAbs()
{
    var x := Abs(-3);
    assert x >= 0;  // ✓ succeeds
    assert x == 3;  // ✗ fails
}

Dafny can prove the first assertion, but it cannot prove the stronger fact that x should not just be some non-negative integer, but exactly 3. As far as Dafny is concerned, all Abs guarantees is that its output is greater than or equal to zero. Notice that this postcondition would still hold if instead Abs was defined to be ‘Abs plus three’.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
method Abs(x: int) returns (result: int)
    ensures result >= 0  // ✓ still succeeds!
{
    if x < 0 {
        result := -x;
    } else {
        result := x;
    }
    result := result + 3;
    // or even `result := 0`!
}

That’s a big problem! But we can fix it easily by adding more postconditions that explain in more detail what Abs guarantees.

For any \(x \in \Z\), we know that \(\lvert x \rvert\) has to be one of exactly two possible values: \(x\) or \(-x\). Let’s add this as a postcondition.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
method Abs(x: int) returns (result: int)
    ensures result >= 0
    ensures result == x || result == -x
{
    if x < 0 {
        result := -x;
    } else {
        result := x;
    }
}

Notice that Dafny can now prove both assertions.

Alternatively, note that we know the exact conditions under which \(\lvert x \rvert\) is \(x\) or \(-x\) respectively. Specifically, we know that \(\lvert x \rvert = x\) when \(x \ge 0\) and that \(\lvert x \rvert = -x\) whenever \(x < 0\).

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
method Abs(x: int) returns (result: int)
    ensures result >= 0
    ensures x >= 0 ==> result == x
    ensures x < 0  ==> result == -x
{
    if x < 0 {
        result := -x;
    } else {
        result := x;
    }
}

Dafny can automatically verify these postconditions and both assertions.

Question 1

Write and verify a method which computes the maximum of two integers. Use the following as a template. You should provide the weakest precondition and the strongest postcondition for full marks. All the tests in TestMax should pass. 

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
method Max(a: int, b: int) returns (m: int)
{
    // todo
}

method {:test} TestMax()
{
    var x := Max(2, 3);
    assert x == 3;

    var y := Max(-4, 1);
    assert y == 1;

    var z := Max(0, 0);
    assert z == 0;
}

Question 2

Write and verify a method which computes the minimum of two integers. Use the following as a template. You should provide the weakest precondition and the strongest postcondition for full marks. All the tests in TestMin should pass.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
method Min(a: int, b: int) returns (m: int)
{
    // todo
}

method {:test} TestMin()
{
    var x := Min(2, 3);
    assert x == 2;

    var y := Min(-4, 1);
    assert y == -4;

    var z := Min(0, 0);
    assert z == 0;
}

Question 3

Decide what the methods M1 and A1 do and provide an appropriate postcondition for each. Verify the program using Dafny.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
method M1(x: int, y: int) returns (r: int)
    // ensures r == ?
    decreases x < 0, x
{
    if x == 0 {
        r := 0;
    } else if x < 0 {
        r := M1(-x, y);
        r := -r;
    } else {
        r := M1(x - 1, y);
        r := A1(r, y);
    }
}

method A1(x: int, y: int) returns (r: int)
    // ensures r == ?
{
    r := x;
    if y < 0 {
        var n := y;
        while n != 0
            invariant r == x + y - n
            invariant -n >= 0
        {
            r := r - 1;
            n := n + 1;
        }
    } else {
        var n := y;
        while n != 0
            invariant r == x + y - n
            invariant n >= 0
        {
            r := r + 1;
            n := n - 1;
        }
    }
}

Question 4

Write a method that swaps the values a[i] and a[j] in-place. This method will modify a, so we have to declare that with the frame condition modifies a. (A frame condition for a method just describes what can and cannot be modified by that method. Dafny assumes that methods do not modify anything, unless you say otherwise.)

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
method swap(a: array<int>, i: nat, j: nat)
    modifies a

    // requires relationship between i and a.Length
    // requires relationship between j and a.Length

    ensures a[i] == old(a[j])
    ensures a[j] == old(a[i])
{
    // todo
}

method {:main} TestSwap()
{
    var a := new int[] [1, 2, 3, 4];

    assert a[1] == 2 && a[3] == 4;
    swap(a, 1, 3);
    assert a[1] == 4 && a[3] == 2;
}