edit

assert s2 + s4 == {1,2,3,4}; // set union

assert s2 * s3 == {1,2} && s2 * s4 == {1}; // set intersection

assert s2 - s3 == {3}; // set difference

Note that because sets can only contain at most one of each element, the union does not count repeated elements more than once. These operators will result in a finite set if both operands are finite, so they cannot generate an infinite set. Unlike the arithmetic operators, the set operators are always defined. In addition to set forming operators, there are comparison operators with their usual meanings:

edit

assert {1} <= {1, 2} && {1, 2} <= {1, 2}; // subset

assert {} < {1, 2} && !({1} < {1}); // strict, or proper, subset

assert !({1, 2} <= {1, 4}) && !({1, 4} <= {1, 4}); // no relation

assert {1, 2} == {1, 2} && {1, 3} != {1, 2}; // equality and non-equality

Sets, like sequences, support the in and !in operators, to test element membership. For example:

edit

assert 5 in {1,3,4,5};

assert 1 in {1,3,4,5};

assert 2 !in {1,3,4,5};

assert forall x :: x !in {};

Sets are used in several annotations, including reads and modifies clauses. In this case, they can be sets of a specific object type (like Nodes in a linked list), or they can be sets of the generic reference type object. Despite its name, this can point to any object or array. This is useful to bundle up all of the locations that a function or method might read or write when they can be different types.

When used in a decreases clause, sets are ordered by subset. This is unlike sequences, which are ordered by length only. In order for sets to be used in decreases clauses, the successive values must be "related" in some sense, which usually implies that they are recursively calculated, or similar.

This requirement comes from the fact that there is no way to get the cardinality (size) of a set in Dafny. The size is guaranteed to be some finite natural, but it is inaccessible. You can test if the set is empty by comparing it to the empty set (s == {} is true if and only if s has no elements.)

A useful way to create sets is using a set comprehension. This defines a new set by including f(x)in the set for all x of type T that satisfy p(x):

set x: T | p(x) :: f(x)

This defines a set in a manner reminiscent of a universal quantifier (forall). As with quanifiers, the type can usually be inferred. In contrast to quantifiers, the bar syntax (|) is required to seperate the predicate (p) from the bound variable (x). The type of the elements of the resulting set is the type of the return value of f(x). The values in the constructed set are the return values of f(x): x itself acts only as a bridge between the predicate p and the function f. It usually has the same type as the resulting set, but it does not need to. As an example:

edit

assert (set x | x in {0,1,2} :: x * 1) == {0,1,2};

If the function is the identity, then the expression can be written with a particularly nice form:

edit

assert (set x | x in {0,1,2,3,4,5} && x < 3) == {0,1,2};

General, non-identity functions in set comprehensions confuse Dafny easily. For example, the following is true, but Dafny cannot prove it:

edit

assert (set x | x in {0,1,2} :: x + 1) == {1,2,3};

This mechanism has the potential to create an infinite set, which is not allowed in Dafny. To prevent this, Dafny employs heuristics in an attempt to prove that that the resulting set will be finite. When creating sets of integers, this can be done by bounding the integers in at least one clause of the predicate (something like 0 <= x < n). Requiring a bound variable to be in an existing set also works, as in x in {0,1,2} from above. This works only when the inclusion part is conjuncted (&&'ed) with the rest of the predicate, as it needs to limit the possible values to consider.

Sequences

Sequences are a built-in Dafny type representing an ordered list. They can be used to represent many ordered collections, including lists, queues, stacks, etc. Sequences are an immutable value type: they cannot be modified once they are created. In this sense, they are similar to strings in languages like Java and Python, except they can be sequences of arbitrary types, rather than only characters. Sequence types are written:

seq<int>

for a sequence of integers, for example. (Note a known bug in Dafny prevents you from creating sequences of naturals, nat.) For example, this function takes a sequence as a parameter:

edit

function sorted(s: seq<int>): bool

{

forall i,j :: 0 <= i < j < |s| ==> s[i] <= s[j]

}

The length of a sequence is written |s|, as in the above quantifier. Specific elements of a sequence are accessed using the same square bracket syntax as arrays. Note also that the function does not require a reads clause to access the sequence. That is because sequences are not stored on the heap; they are values, so functions don't need to declare when they are accessing them. The most powerful property of sequences is the fact that annotations and functions can create and manipulate them. For example, another way of expressing sorted-ness is recursive: if the first element is smaller than the rest, and the rest is sorted, then the whole array is sorted:

edit

function sorted2(s: seq<int>): bool

{

0 < |s| ==> (forall i :: 0 < i < |s| ==> s[0] <= s[i]) &&

sorted2(s[1..])

}

The notation s[1..] is slicing the sequence. It means starting at the first element, take elements until you reach the end. This does not modify s, as sequences are immutable. Rather, it creates a new sequence which has all the same elements in the same order, except for the first one. This is similar to addition of integers in that the original values are not changed, just new ones created. The slice notation is:

s[i..j]

where 0 <= i <= j <= |s|. Dafny will enforce these index bounds. The resulting sequence will have exactly j-i elements, and will start with the element s[i] and continue sequentially through the sequence, if the result is non-empty. This means that the element at index j is excluded from the slice, which mirrors the same half-open interval used for regular indexing.

Sequences can also be constructed from their elements, using display notation:

var s := [1, 2, 3];

Here we have a integer sequence variable in some imperative code containing the elements 1,2, and 3. Type inference has been used here to get the fact that the sequence is one of integers. This notation allows us to construct empty sequences and singleton sequences:

[] // the empty sequence, which can be a sequence of any type

[true] // a singleton sequence of type seq

Slice notation and display notation can be used to check properties of sequences:

edit

var s := [1, 2, 3, 4, 5];

assert s[|s|-1] == 5; //access the last element

assert s[|s|-1..|s|] == [5]; //slice just the last element, as a singleton

assert s[1..] == [2, 3, 4, 5]; // everything but the first

assert s[..|s|-1] == [1, 2, 3, 4]; // everything but the last

assert s == s[0..] == s[..|s|] == s[0..|s|] == s[..]; // the whole sequence

By far the most common operations on sequences are getting the first and last elements, and getting everything but the first and last elements, as these are often used in recursive functions, such as sorted2 above. In addition to being deconstructed by being accessed or sliced, sequences can also be concatenated, using the plus (+) symbol:

edit

assert [1,2,3] == [1] + [2,3];

assert s == s + [];

assert forall i :: 0 <= i <= |s| ==> s == s[..i] + s[i..];

The second assertion gives a relationship between concatenation and slicing. Because the slicing operation is exclusive on one side and inclusive on the other, the element appears in the concatenation exactly once, as it should. Note that the concatenation operation is associative:

edit

assert forall a: seq<int>, b: seq<int>, c: seq<int> ::

(a + b) + c == a + (b + c);

but that the Z3 theorem prover will not realize this unless it is prompted with an assertion stating that fact (see Lemmas/Induction for more information on why this is necessary).

Sequences also support the in and !in operators, which test for containment within a sequence:

edit

assert 5 in s; // using s from before

assert 0 !in s;

This also allows us an alternate means of quantifying over the elements of a sequence, when we don't care about the index. For example, we can require that a sequence only contains elements which are indices into the sequence:

edit

var p := [2,3,1,0];

assert forall i :: i in p ==> 0 <= i < |s|;

This is a property of each individual element of the sequence. If we wanted to relate multiple elements to each other, we would need to quantify over the indices, as in the first example.

Sometimes we would like to emulate the updatable nature of arrays using sequences. While we can't change the original sequence, we can create a new sequence with the same elements everywhere except for the updated element:

edit

s[i := v] // replace index i by v in seq s

Of course, the index i has to be an index into the array. This syntax is just a shortcut for an operation that can be done with regular slicing and access operations. Can you fill in the code below that does this?

edit

function update(s: seq<int>, i: int, v: int): seq<int>

requires 0 <= index < |s|;

ensures update(s, i, v) == s[i := v];

{

// open in the editor to see the answer.

}

You can also form a sequence from the elements of an array. This is done using the same "slice" notation as above:

edit

var a := new int[3]; // 3 element array of ints

a[0], a[1], a[2] := 0, 3, -1;

var s := a[..];

assert s == [0, 3, -1];

To get just part of the array, the bounds can be given just like in a regular slicing operation:

edit

assert a[1..] == [3, -1];

assert a[..1] == [0];

assert a[1..2] == [3];

Because sequences support in and !in, this operation gives us an easy way to express the "element not in array" property, turning:

forall k :: 0 <= k < a.Length ==> elem != a[k]

into:

elem !in a[..]

Further, bounds are easily included:

forall k :: 0 <= k < i ==> elem != a[k]

is the same as

elem !in a[..i]

Lemmas and Induction

1. Introduction

2. Searching for Zero

3. Lemmas

4. Counting

5. Proving the Distributive Property

6. Induction

7. Function Lemmas

Introduction

Sometimes there are steps of logic required to prove a program correct, but they are too complex for Dafny to discover and use on its own. When this happens, we can often give Dafny assistance by providing a lemma.

Lemmas are theorems used to prove another result, rather than being a goal in and of themselves. They allow Dafny to break the proof into two: prove the lemma, then use it to prove the final result; the final result being the correctness of the program. By splitting it in this way, you can prevent Dafny from trying to bite off more than it can chew. Dafny, and computers in general, is very good a dealing with a bunch of specific details and covering all the cases, but it lacks the cleverness to see intermediate steps that make the proof process easier.

By writing and using lemmas, you can point out what these steps are, and when to use them in a program. The are particularly important for inductive arguments, which are some of the hardest problems for theorem provers.

Searching for Zero

As our first look at lemmas, we will consider a somewhat contrived example: searching for zero in an array. What makes this problem interesting is that the array we are searching in has two special properties: all elements are non-negative, and each successive element decreases by at most one from the previous element. In code:

edit