Dafny - guide

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

method Abs(x: int) returns (y: int)
{
   ...
}

method MultipleReturns(x: int, y: int) returns (more: int, less: int)
{
   ...
}

method MultipleReturns(x: int, y: int) returns (more: int, less: int)
{
   more := x + y;
   less := x - y;
   // comments: are not strictly necessary.
}

method Abs(x: int) returns (y: int)
{
   if x < 0
      { return -x; }
   else
      { return x; }
}

method Abs(x: int) returns (y: int)
   ensures 0 <= y
{
   ...
}

method MultipleReturns(x: int, y: int) returns (more: int, less: int)
   ensures less < x
   ensures x < more
{
   more := x + y;
   less := x - y;
}

   ensures less < x && x < more

   ensures less < x < more

method MultipleReturns(x: int, y: int) returns (more: int, less: int)
   requires 0 < y
   ensures less < x < more
{
   more := x + y;
   less := x - y;
}

method Max(a: int, b:int) returns (c: int)

method Testing()
{
   assert 2 < 3;
}

   var x: int := 5;

   var x := 5;

   var x, y, z: bool := 1, 2, true;

// use definition of Abs() from before.
method Testing()
{
   var v := Abs(3);
   assert 0 <= v;
}

method Testing() { ... }

   assert v == 3;

method Abs(x: int) returns (y: int)
   ensures 0 <= y
{
   y := 0;
}

   var v := Abs(3);
   assert v == 3;

method Abs(x: int) returns (y: int)
   ensures 0 <= y
   ensures 0 <= x ==> x == y
{
   // body as before
}

method Abs(x: int) returns (y: int)
   ensures 0 <= y
   ensures 0 <= x ==> x == y
   ensures x < 0 ==> y == -x
{
   // body as before
}

   ensures 0 <= y && (y == x || y == -x)

method Abs(x: int) returns (y: int) { ... }

method Abs(x: int) returns (y: int) { ... }

function abs(x: int): int
{
   ...
}

function abs(x: int): int
{
   if x < 0 then -x else x
}

   assert abs(3) == 3;

function max(a: int, b: int): int { ... }

One caveat of functions is that not only can they appear in annotations, they can only appear in annotations. One cannot write:

   var v := abs(3);

as this is not an annotation. Functions are never part of the final compiled program, they are just tools to help us verify our code. Sometimes it is convenient to use a function in real code, so one can define a function method, which can be called from real code. Note that there are restrictions on what functions can be function methods (See the reference for details).

Exercise 5. Change your test method from Exercise 4 to capture the value of max to a variable, and then do the checks from Exercise 4 using the variable. Dafny will reject this program because you are calling max from real code. Fix this problem using a function method.

function max(a: int, b: int): int { ... }

Exercise 6. Now that we have an abs function, change the postcondition of method Abs to make use of abs. After confirming the method still verifies, change the body of Abs to also use abs. (After doing this, you will realize there is not much point in having a method that does exactly the same thing as a function method.)

function abs(x: int): int

Unlike methods, functions can appear in expressions. Thus we can do something like implement the mathematical Fibonacci function:

function fib(n: nat): nat
{
   if n == 0 then 0 else
   if n == 1 then 1 else
                  fib(n - 1) + fib(n - 2)
}

Here we use nats, the type of natural numbers (non-negative integers), which is often more convenient than annotating everything to be non-negative. It turns out that we could make this function a function method if we wanted to. But this would be extremely slow, as this version of calculating the Fibonacci numbers has exponential complexity. There are much better ways to calculate the Fibonacci function. But this function is still useful, as we can have Dafny prove that a fast version really matches the mathematical definition. We can get the best of both worlds: the guarantee of correctness and the performance we want.

We can start by defining a method like the following:

method ComputeFib(n: nat) returns (b: nat)
   ensures b == fib(n)
{
}

We haven't written the body yet, so Dafny will complain that our post condition doesn't hold. We need an algorithm to calculate the n^th Fibonacci number. The basic idea is to keep a counter, and repeatedly calculate adjacent pairs of Fibonacci numbers until the desired number is reached. To do this, we need a loop. In Dafny, this is done via a while loop. A while loop looks like the following:

   var i := 0;
   while i < n
   {
      i := i + 1;
   }

This is a trivial loop that just increments i until it reaches n. This will form the core of our loop to calculate Fibonacci numbers.

Loop Invariants

While loops present a problem for Dafny. There is no way for Dafny to know in advance how many times the code will go around the loop. But Dafny needs to consider all paths through a program, which could include going around the loop any number of times. To make it possible for Dafny to work with loops, you need to provide loop invariants, another kind of annotation.

A loop invariant is an expression that holds upon entering a loop, and after every execution of the loop body. It captures something that is invariant, i.e. does not change, about every step of the loop. Now, obviously we are going to want to change variables, etc. each time around the loop, or we wouldn't need the loop. Like pre- and postconditions, an invariant is a property that is preserved for each execution of the loop, expressed using the same boolean expressions we have seen. For example, we see in the above loop that if i starts off positive, then it stays positive. So we can add the invariant, using its own keyword, to the loop:

   var i := 0;
   while i < n
      invariant 0 <= i
   {
      i := i + 1;
   }

When you specify an invariant, Dafny proves two things: the invariant holds upon entering the loop, and it is preserved by the loop. By preserved, we mean that assuming that the invariant holds at the beginning of the loop, we must show that executing the loop body once makes the invariant hold again. Dafny can only know upon analyzing the loop body what the invariants say, in addition to the loop guard (the loop condition). Just as Dafny will not discover properties of a method on its own, it will not know any but the most basic properties of a loop are preserved unless it is told via an invariant.

In our example, the point of the loop is to build up the Fibonacci numbers one (well, two) at a time until we reach the desired number. After we exit the loop, we will have that i == n, because i will stop being incremented when it reaches n. We can use our assertion trick to check to see if Dafny sees this fact as well:

   var i: int := 0;
   while i < n
      invariant 0 <= i
   {
      i := i + 1;
   }
   assert i == n;

We find that this assertion fails. As far as Dafny knows, it is possible that i somehow became much larger than n at some point during the loop. All it knows after the loop exits (i.e. in the code after the loop) is that the loop guard failed, and the invariants hold. In this case, this amounts to n <= i and 0 <= i. But this is not enough to guarantee that i == n, just that n <= i. Somehow we need to eliminate the possibility of i exceeding n. One first guess for solving this problem might be the following:

   var i := 0;
   while i < n
      invariant 0 <= i < n
   {
      i := i + 1;
   }

This does not verify, as Dafny complains that the invariant is not preserved (also known as not maintained) by the loop. We want to be able to say that after the loop exits, then all the invariants hold. Our invariant holds for every execution of the loop except for the very last one. Because the loop body is executed only when the loop guard holds, in the last iteration i goes from n - 1 to n, but does not increase further, as the loop exits. Thus, we have only omitted exactly one case from our invariant, and repairing it relatively easy:

...
   invariant 0 <= i <= n
...

Now we can say both that n <= i from the loop guard and 0 <= i <= n from the invariant, which allows Dafny to prove the assertion i == n. The challenge in picking loop invariants is finding one that is preserved by the loop, but also that lets you prove what you need after the loop has executed.

Exercise 7. Change the loop invariant to 0 <= i <= n+2. Does the loop still verify? Does the assertion i == n after the loop still verify?

   invariant 0 <= i <= n+2

Exercise 8. With the original loop invariant, change the loop guard from i < n to i != n. Do the loop and the assertion after the loop still verify? Why or why not?

   while i != n ...

In addition to the counter, our algorithm called for a pair of numbers which represent adjacent Fibonacci numbers in the sequence. Unsurprisingly, we will have another invariant or two to relate these numbers to each other and the counter. To find these invariants, we employ a common Dafny trick: working backwards from the postconditions.

Our postcondition for the Fibonacci method is that the return value b is equal to fib(n). But after the loop, we have that i == n, so we need b == fib(i) at the end of the loop. This might make a good invariant, as it relates something to the loop counter. This observation is surprisingly common throughout Dafny programs. Often a method is just a loop that, when it ends, makes the postcondition true by having a counter reach another number, often an argument or the length of an array or sequence. So we have that the variable b, which is conveniently our out parameter, will be the current Fibonacci number:

   invariant b == fib(i)

We also note that in our algorithm, we can compute any Fibonacci number by keeping track of a pair of numbers, and summing them to get the next number. So we want a way of tracking the previous Fibonacci number, which we will call a. Another invariant will express that number's relation to the loop counter. The invariants are:

   invariant a == fib(i - 1)

At each step of the loop, the two values are summed to get the next leading number, while the trailing number is the old leading number. Using a parallel assignment, we can write a loop that performs this operation:

   var i := 1;
   var a := 0;
       b := 1;
   while i < n
      invariant 0 < i <= n
      invariant a == fib(i - 1)
      invariant b == fib(i)
   {
      a, b := b, a + b;
      i := i + 1;
   }

Here a is the trailing number, and b is the leading number. The parallel assignment means that the entire right hand side is calculated before the assignments to the variables are made. Thus a will get the old value of b, and b will get the sum of the two old values, which is precisely the behavior we want.

We also have made a change to the loop counter i. Because we also want to track the trailing number, we can't start the counter at zero, as otherwise we would have to calculate a negative Fibonacci number. The problem with doing this is that the loop counter invariant may not hold when we enter the loop. The only problem is when n is zero. This can be eliminated as a special case, by testing for this condition at the beginning of the loop. The completed Fibonacci method becomes:

method ComputeFib(n: nat) returns (b: nat)
   ensures b == fib(n)
{
   if n == 0 { return 0; }
   var i: int := 1;
   var a := 0;
       b := 1;
   while i < n
      invariant 0 < i <= n
      invariant a == fib(i - 1)
      invariant b == fib(i)
   {
      a, b := b, a + b;
      i := i + 1;
   }
}

Dafny no longer complains about the loop invariant not holding, because if n were zero, it would return before reaching the loop. Dafny is also able to use the loop invariants to prove that after the loop, i == n and b == fib(i), which together imply the postcondition, b == fib(n).

Exercise 9. The ComputeFib method above is more complicated than necessary. Write a simpler program by not introducing a as the Fibonacci number that precedes b, but instead introducing a variable c that succeeds b. Verify your program is correct according to the mathematical definition of Fibonacci.

method ComputeFib(n: nat) returns (b: nat)

Exercise 10. Starting with the completed ComputeFib method above, delete the if statement and initialize i to 0, a to 1, and b to 0. Verify this new program by adjusting the loop invariants to match the new behavior.

method ComputeFib(n: nat) returns (b: nat)

One of the problems with using invariants is that it is easy to forget to have the loop make progress, i.e. do work at each step. For example, we could have omitted the entire body of the loop in the previous program. The invariants would be correct, because they are still true upon entering the loop, and since the loop doesn't change anything, they would be preserved by the loop. But the crucial step from the loop to the postcondition wouldn't hold. We know that if we exit the loop, then we can assume the negation of the guard and the invariants, but this says nothing about what happens if we never exit the loop. Thus we would like to make sure the loop ends at some point, which gives us a much stronger correctness guarantee (the technical term is total correctness).

Termination

Dafny proves that code terminates, i.e. does not loop forever, by using decreases annotations. For many things, Dafny is able to guess the right annotations, but sometimes it needs to be made explicit. In fact, for all of the code we have seen so far, Dafny has been able to do this proof on its own, which is why we haven't seen the decreases annotation explicitly yet. There are two places Dafny proves termination: loops and recursion. Both of these situations require either an explicit annotation or a correct guess by Dafny.

A decreases annotation, as its name suggests, gives Dafny and expression that decreases with every loop iteration or recursive call. There are two conditions that Dafny needs to verify when using a decreases expression: that the expression actually gets smaller, and that it is bounded. Many times, an integral value (natural or plain integer) is the quantity that decreases, but other things that can be used as well. (See the reference for details.) In the case of integers, the bound is assumed to be zero. For example, the following is a proper use of decreases on a loop (with its own keyword, of course):

   while 0 < i
      invariant 0 <= i
      decreases i
   {
      i := i - 1;
   }

Here Dafny has all the ingredients it needs to prove termination. The variable i gets smaller each loop iteration, and is bounded below by zero. This is fine, except the loop is backwards from most loops, which tend to count up instead of down. In this case, what decreases is not the counter itself, but rather the distance between the counter and the upper bound. A simple trick for dealing with this situation is given below:

   while i < n
      invariant 0 <= i <= n
      decreases n - i
   {
      i := i + 1;
   }

This is actually Dafny's guess for this situation, as it sees i < n and assumes that n - i is the quantity that decreases. The upper bound of the loop invariant implies that 0 <= n – i, and gives Dafny a lower bound on the quantity. This also works when the bound n is not constant, such as in the binary search algorithm, where two quantities approach each other, and neither is fixed.

Exercise 11. In the loop above, the invariant i <= n and the negation of the loop guard allow us to conclude i == n after the loop (as we checked previously with an assert. Note that if the loop guard were instead written as i != n (as in Exercise 8), then the negation of the guard immediately gives i == n after the loop, regardless of the loop invariant. Change the loop guard to i != n and delete the invariant annotation. Does the program verify? What happened?

   while i != n

The other situation that requires a termination proof is when methods or functions are recursive. Similarly to looping forever, these methods could potentially call themselves forever, never returning to their original caller. When Dafny is not able to guess the termination condition, an explicit decreases clause can be given along with pre- and postconditions, as in the unnecessary annotation for the fib function:

function fib(n: nat): nat
   decreases n
{
   ...
}

As before, Dafny can guess this condition on its own, but sometimes the decreasing condition is hidden within a field of an object or somewhere else where Dafny cannot find it on its own, and it requires an explicit annotation.

Arrays

All that we have considered is fine for toy functions and little mathematical exercises, but it really isn't helpful for real programs. So far we have only considered a handful of values at a time in local variables. Now we turn our attention to arrays of data. Arrays are a built in part of the language, with their own type, array<T>, where T is another type. For now we only consider arrays of integers, array<int>. Arrays can be null, and have a built in length field, a.Length. Element access uses the standard bracket syntax and are indexed from zero, so a[3] is preceded by the 3 elements a[0], a[1], and a[2], in that order. All array accesses must be proven to be within bounds, which is part of the no-runtime-errors safety guarantee by Dafny. Because bounds checks are proven at verification time, no runtime checks need to be made. To create a new array, it must be allocated with the new keyword, but for now we will only work with methods that take a previously allocated array as an argument. (See the tutorial on memory for more on allocation.)

One of the most basic things we might want to do with an array is search through it for a particular key, and return the index of a place where we can find the key if it exists. We have two outcomes for a search, with a different correctness condition for each. If the algorithm returns an index (i.e. non-negative integer), then the key should be present at that index. This might be expressed as follows:

method Find(a: array<int>, key: int) returns (index: int)
   ensures 0 <= index ==> index < a.Length && a[index] == key
{
   // Open in editor for a challenge...
}

The array index here is safe because the implication operator is short circuiting. Short circuiting means if the left part is false, then the implication is already true regardless of the truth value of the second part, and thus it does not need to be evaluated. Using the short circuiting property of the implication operator, along with the boolean "and" (&&), which is also short circuiting, is a common Dafny practice. The condition index < a.Length is necessary because otherwise the method could return a large integer which is not an index into the array. Together, the short circuiting behavior means that by the time control reaches the array access, index must be a valid index.

If the key is not in the array, then we would like the method to return a negative number. In this case, we want to say that the method did not miss an occurrence of the key; in other words, that the key is not in the array. To express this property, we turn to another common Dafny tool: quantifiers.

Quantifiers

A quantifier in Dafny most often takes the form of a forall expression, also called a universal quantifier. As its name suggests, this expression is true if some property holds for all elements of some set. For now, we will consider the set of integers. An example universal quantifier, wrapped in an assertion, is given below:

   assert forall k :: k < k + 1;

A quantifier introduces a temporary name for each element of the set it is considering. This is called the bound variable, in this case k. The bound variable has a type, which is almost always inferred rather than given explicitly and is usually int anyway. (In general, one can have any number of bound variables, a topic we will return to later). A pair of colons (::) separates the bound variable and its optional type from the quantified property (which must be of type bool). In this case, the property is that adding one to any integer makes a strictly larger integer. Dafny is able to prove this simple property automatically. Generally it is not very useful to quantify over infinite sets, such as all the integers. Instead, quantifiers are typically used to quantify over all elements in an array or data structure. We do this for arrays by using the implication operator to make the quantified property trivially true for values which are not indices:

   assert forall k :: 0 <= k < a.Length ==> ...a[k]...;

This says that some property holds for each element of the array. The implication makes sure that k is actually a valid index into the array before evaluating the second part of the expression. Dafny can use this fact not only to prove that the array is accessed safely, but also reduce the set of integers it must consider to only those that are indices into the array.

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 postconditions become (with the addition of the non-nullity precondition on a):

method Find(a: array<int>, key: int) returns (index: int)
   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:

   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 postconditions. 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 postcondition, we can use a quantifier to express this property:

   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:

method Find(a: array<int>, key: int) returns (index: int)
   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;
}

Exercise 12. Write a method that takes an integer array, which it requires to have at least one element, and returns an index to the maximum of the array's elements. Annotate the method with pre- and postconditions that state the intent of the method, and annotate its body with loop invariant to verify it.

method FindMax(a: array<int>) returns (i: int)

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, "if x is before 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:

predicate sorted(a: array<int>)
   requires a != null
{
   forall j, k :: 0 <= j < k < a.Length ==> a[j] <= a[k]
}

Note that there is no return type, because predicates always return a boolean.

Dafny rejects this code as given, claiming that the predicate 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 (or predicate) 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.

predicate sorted(a: array<int>)
   ...
   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 postconditions. 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. 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 that are not memory locations 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 reads cousins, 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 reads 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.)

Exercise 13. Modify the definition of the sorted predicate so that it returns true exactly when the array is sorted and all its elements are distinct.

predicate sorted(a: array<int>)

Exercise 14. What happens if you remove the precondition a != null? Change the definition of sorted so that it allows its argument to be null but returns false if it is.

predicate sorted(a: array<int>)

Binary Search

Predicates are usually used to make other annotations clearer:

method BinarySearch(a: array<int>, key: int) returns (index: int)
   requires a != null && sorted(a)
   ensures ...
{
   ...
}

We have the same postconditions 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:

   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 postcondition 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.

Exercise 15. Change the assignments in the body of BinarySearch to set low to mid or to set high to mid - 1. In each case, what goes wrong?

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

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 postconditions, and writing assertions to check assumptions are all general computer science skills that will benefit you no matter what language you work in.