Dafny - guide (811281), страница 3

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 3)

{

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:

edit

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 ton, 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:

edit

...

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.

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 post-conditions.

Our post-condition 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 post-condition 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:

edit

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:

edit

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 post-condition, b == fib(n).

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 post-condition 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):

edit

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:

edit

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.

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 post-conditions, as in the unnecessary annotation for the fib function:

edit

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:

edit

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

requires ...

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:

edit

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

Характеристики

Список файлов книги