With a quantifier, saying the key is not in the array is straightforward:

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

Thus our method post-conditions become (with the addition of the non-nullity pre-condition ona):

edit

method Find(a: array<int>, key: int) returns (index: int)

requires a != null;

ensures 0 <= index ==> index < a.Length && a[index] == key;

ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != key;

{

...

}

We can fill in the body of this method in a number of ways, but perhaps the easiest is a linear search, implemented below:

edit

index := 0;

while (index < a.Length)

{

if (a[index] == key) { return; }

index := index + 1;

}

index := -1;

As you can see, we have omitted the loop invariants on the while loop, so Dafny gives us a verification error on one of the post-conditions. The reason we get an error is that Dafny does not know that the loop actually covers all the elements. In order to convince Dafny of this, we have to write an invariant that says that everything before the current index has already been looked at (and are not the key). Just like the post-condition, we can use a quantifier to express this property:

edit

invariant forall k :: 0 <= k < index ==> a[k] != key;

This says that everything before, but excluding, the current index is not the key. Notice that upon entering the loop, i is zero, so the first part of the implication is always false, and thus the quantified property is always true. This common situation is known as vacuous truth: the quantifier holds because it is quantifying over an empty set of objects. This means that it is true when entering the loop. We test the value of the array before we extend the non-key part of the array, so Dafny can prove that this invariant is preserved. One problem arises when we try to add this invariant: Dafny complains about the index being out of range for the array access within the invariant.

This is code does not verify because there is no invariant on index, so it could be greater than the length of the array. Then the bound variable, k, could exceed the length of the array. To fix this, we put the standard bounds on index, 0 <= index <= a.Length. Note that because we say k <index, the array access is still protected from error even when index == a.Length. The use of a variable that is one past the end of a growing range is a common pattern when working with arrays, where it is often used to build a property up one element at a time. The complete method is given below:

edit

method Find(a: array<int>, key: int) returns (index: int)

requires a != null;

ensures 0 <= index ==> index < a.Length && a[index] == key;

ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != key;

{

index := 0;

while (index < a.Length)

invariant 0 <= index <= a.Length;

invariant forall k :: 0 <= k < index ==> a[k] != key;

{

if (a[index] == key) { return; }

index := index + 1;

}

index := -1;

}

A linear search is not very efficient, especially when many queries are made of the same data. If the array is sorted, then we can use the very efficient binary search procedure to find the key. But in order for us to be able to prove our implementation correct, we need some way to require that the input array actually is sorted. We could do this directly with a quantifier inside a requires clause of our method, but a more modular way to express this is through a predicate.

Predicates

A predicate is a function which returns a boolean. It is a simple but powerful idea that occurs throughout Dafny programs. For example, we define the sorted predicate over arrays of integers as a function that takes an array as an argument, and returns true if and only if that array is sorted in increasing order. The use of predicates makes our code shorter, as we do not need to write out a long property over and over. It can also make our code easier to read by giving a common property a name.

There are a number of ways we could write the sorted predicate, but the easiest is to use a quantifier over the indices of the array. We can write a quantifier that expresses the property, "ifx</span> is before <c>y in the array, then x <= y," as a quantifier over two bound variables:

forall j, k :: 0 <= j < k < a.Length ==> a[j] <= a[k]

Here we have two bound variables, j and k, which are both integers. The comparisons between the two guarantee that they are both valid indices into the array, and that j is before k. Then the second part says that they are ordered properly with respect to one another. Quantifiers are just a type of boolean valued expression in Dafny, so we can write the sorted predicate as:

edit

function sorted(a: array<int>): bool

requires a != null;

{

forall j, k :: 0 <= j < k < a.Length ==> a[j] <= a[k]

}

Dafny rejects this code as given, claiming that the function cannot read a. Fixing this issue requires another annotation, the reads annotation.

Framing

The sorted predicate is not able to access the array because the array was not included in the function's reading frame. The reading frame of a function is all the memory locations that the function is allowed to read. The reason we might limit what a function can read is so that when we write to memory, we can be sure that functions that did not read that part of memory have the same value they did before. For example, we might have two arrays, one of which we know is sorted. If we did not put a reads annotation on the sorted predicate, then when we modify the unsorted array, we cannot determine whether the other array stopped being sorted. While we might be able to give invariants to preserve it in this case, it gets even more complex when manipulating data structures. In this case, framing is essential to making the verification process feasible.

edit

function sorted(a: array<int>): bool

...

reads a;

...

A reads annotation is not a boolean expression, like the other annotations we have seen, and can appear anywhere along with the pre- and post-conditions. Instead of a property that should be true, it specifies a set of memory locations that the function is allowed to access. The name of an array, like a in the above example, stands for all the elements of that array. One can also specify object fields and sets of objects, but we will not concern ourselves with those topics here. (See the framing tutorial for details.) Dafny will check that you do not read any memory location that is not stated in the reading frame. This means that function calls within a function must have reading frames that are a subset of the calling function's reading frame. One thing to note is that parameters to the function are not memory locations, so do not need to be declared.

Frames also affect methods. As you might have guessed, they are not required to list the things they read, as we have written a method which accesses an array with no reads annotation. Methods are allowed to read whatever memory they like, but they are required to list which parts of memory they modify, with a modifies annotation. They are almost identical to their readscousins, except they say what can be changed, rather than what the value of the function depends on. In combination with reads, modification restrictions allow Dafny to prove properties of code that would otherwise be very difficult or impossible. Reads and modifies are one of the tools that allow Dafny to work on one method at a time, because they restrict what would otherwise be arbitrary modifications of memory to something that Dafny can reason about.

Note that framing only applies to the heap, or memory accessed through references. Local variables are not stored on the heap, so they cannot be mentioned in annotations. Note also that types like sets, sequences, and multisets are value types, and are treated like integers or local variables. Arrays and objects are reference types, and they are stored on the heap (though as always there is a subtle distinction between the reference itself and the value it points to; see the data structure tutorial for details.)

Binary Search

Predicates are usually used to make other annotations clearer:

edit

method BinarySearch(a: array<int>, key: int) returns (index: int)

requires a != null && sorted(a);

ensures ...;

{

...

}

We have the same post-conditions that we did for the linear search, as the goal is the same. The difference is that now we know the array is sorted. Because Dafny can unwrap functions, inside the body of the method it knows this too. We can then use that property to prove the correctness of the search. The method body is given below:

edit

var low, high := 0, a.Length;

while (low < high)

invariant 0 <= low <= high <= a.Length;

invariant forall i ::

0 <= i < a.Length && !(low <= i < high) ==> a[i] != value;

{

var mid := (low + high) / 2;

if (a[mid] < value)

{

low := mid + 1;

}

else if (value < a[mid])

{

high := mid;

}

else

{

return mid;

}

}

return -1;

This is a fairly standard binary search implementation. First we declare our range to search over. This can be thought of as the remaining space where the key could possibly be. The range is inclusive-exclusive, meaning it encompasses indices [low, high). The first invariant expresses the fact that this range is within the array. The second says that the key is not anywhere outside of this range. In the first two branches of the if chain, we find the element in the middle of our range is not the key, and so we move the range to exclude that element and all the other elements on the appropriate side of it. We need the addition of one when moving the lower end of the range because it is inclusive on the low side. If we do not add one, then the loop may continue forever when mid == low, which happens when low + 1 == high. We could change this to say that the loop exits when low and high are one apart, but this would mean we would need an extra check after the loop to determine if the key was found at the one remaining index. In the above formulation, this is unnecessary because when low == high, the loop exits. But this means that no elements are left in the search range, so the key was not found. This can be deduced from the loop invariant:

invariant forall i ::

0 <= i < a.Length && !(low <= i < high) ==> a[i] != value;

When low == high, the negated condition in the first part of the implication is always true (because no i can be both at least and strictly smaller than the same value). Thus the invariant says that all elements in the array are not the key, and the second post-condition holds. As you can see, it is easy to introduce subtle off by one errors in this code. With the invariants, not only can Dafny prove the code correct, but we can understand the operation of the code more easily ourselves.

Conclusion

We've seen a whirlwind tour of the major features of Dafny, and used it for some interesting, if a little on the small side, examples of what Dafny can do. But to really take advantage of the power Dafny offers, on needs to plow ahead into the advanced topics: objects, sequences and sets, data structures, lemmas, etc. Now that you are familiar with the basics of Dafny, you can peruse the tutorials on each of these topics at your leisure. Each tutorial is designed to be a relatively self-contained guide to its topic, though some benefit from reading others beforehand. The examples are also a good place to look for model Dafny programs. Finally, the reference contains the gritty details of Dafny syntax and semantics, for when you just need to know what the disjoint set operator is (it's !!, for those interested).

Even if you do not use Dafny regularly, the idea of writing down exactly what it is that the code does is a precise way, and using this to prove code correct is a useful skill. Invariants, pre- and post- conditions, and annotations are useful in debugging code, and also as documentation for future developers. When modifying or adding to a codebase, they confirm that the guarantees of existing code are not broken. They also ensure that APIs are used correctly, by formalizing behavior and requirements and enforcing correct usage. Reasoning from invariants, considering pre- and post-conditions, and writing assertions to check assumptions are all general computer science skills that will benefit you no matter what language you work in.

Sets

Sets of various types form one of the core tools of verification for Dafny. Sets represent an orderless collection of elements, without repetition. Like sequences, sets are immutable value types. This allows them to be used easily in annotations, without involving the heap, as a set cannot be modified once it has been created. A set has the type:

set<int>

for a set of integers, for example. In general, sets can be of almost any type, including objects. Concrete sets can be specified by using display notation:

edit

var s1 := {}; // the empty set

var s2 := {1, 2, 3}; // set contains exactly 1, 2, and 3

assert s2 == {1,1,2,3,3,3,3}; // same as before

var s3, s4 := {1,2}, {1,4};

The set formed by the display is the expected set, containing just the elements specified. Above we also see that equality is defined for sets. Two sets are equal if they have exactly the same elements. New sets can be created from existing ones using the common set operations: