Dafny Lab Sheet 4

You can skip to the lab questions if you’re in a hurry, but as always I recommend reading the following sections as they give good context for the lab.

Dynamic Frames

Dafny contains a few reference types, mainly arrays and objects. The values pointed to by references are stored on the heap.

Dafny methods are not allowed to modify any heap values by default, but they may modify values stored on the stack, or heap-allocated values local to the method. The set of objects that may be modified by a method is called its frame. We have already seen methods with frames—for example, the swap method in lab 1.

To specify a method’s frame, use a modifies clause. A method that modifies an array a and an object o can be written in any one of the following ways.

1
2
3

modifies a, o
modifies {a, o}
modifies {a} + {o}

Functional code can read the heap state but cannot modify it. Functions and predicates therefore use a reads clause instead of a modifies clause.

Postconditions for methods in Dafny are so-called ‘two-state predicates’, since they have access to the state of the heap before and after a method is executed. The expression old(E) refers to the value of E just before the enlosing method. For example, consider this postcondition for a method that increments each value in an integer array.

1

forall i | 0 <= i < a.Length :: a[i] == old(a[i]) + 1

This says that for each index i, the new value a[i] is equal to the old value of a[i] plus one.

It’s important not to write old(a)[i]. The value a is a reference passed as a parameter to the method and does not change. Think of it like a pointer to the location in memory where the array values are stored. It’s always true that old(a) == a, and therefore old(a)[i] == a[i], since the reference itself can’t be modified. The value a[i], however, is the heap value obtained by dereferencing a. This can change, and hence old(a[i]) may not be equal to a[i].

Classes

Classes in Dafny look exactly like classes in any other object-oriented language. A class is just a list of members of that class—fields, methods, functions.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

class Point2 {
    var x: real, y: real

    constructor(x: real, y: real)
        ensures this.x == x && this.y == y
    {
        this.x := x;
        this.y := y;
    }

    function Dot(other: Point2): real
        reads this, other
    {
        x * other.x + y * other.y
    }
}

method {:main} TestPoint() {
    var p := new Point2(3.0, 4.0);
    var q := new Point2(1.2, -3.5);
    assert p.Dot(q) == -10.4;
    print p.Dot(q), "\n";
}

Question 1

Consider the following class which represents a pointer to an array. It contains a single method InitArray which sets a to a new array of a given size. What does InitArray modify? Explain your answer.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10

class Pointer {
    var a: array<int>

    method InitArray(size: nat)
        // modifies what?
    {
        var b := new int[size];
        a := b;
    }
}

Question 2

Write a method which doubles the values of an array s and stores it in an array t.

1
2
3
4
5
6
7

method DoubleArray(s: array<int>, t: array<int>)
    // needs a frame
    // needs one precondition
    // needs a postcondition saying that t[i] is twice s[i]
{
    // todo
}

Be careful: the input arguments s and t might refer to the same array.

Question 3

Write a method CumulativeSum which updates an array to its cumulative sum. Prove that each new a[i] is equal to the sum old(a[0] + ⋯ + a[i]).

For example, if a = [1, 2, 3, 4] then CumulativeSum(a) should modify a such that a = [1, 3, 6, 10]. You will need the function SumTo provided below which computes the sum of an array’s elements up to but not including a specified index.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12

function SumTo(a: array<int>, i: nat): int
    reads a
    requires 0 <= i <= a.Length
{
    if i == 0 then 0 else SumTo(a, i - 1) + a[i - 1]
}

method CumulativeSum(a: array<int>)
    // needs modifies clause and postcondition
{
    // todo
}