Dafny - guide (Dafny - guide.docx), страница 6

requires forall i :: 0 <= i < a.Length ==> 0 <= a[i];

requires forall i :: 0 < i < a.Length ==> a[i-1]-1 <= a[i];

With these requirements, we can do something clever in our search routine: we can skip elements. Imagine that we are traversing through the array, and we see a[j] == 7. Then we know that 6 <= a[j+1], 5 <= a[j+2], etc. In fact, the next zero can't be until 7 more elements in the array. So we don't even have to search for a zero until a[j+a[j]]. So we could write a loop like:

edit

index := 0;

while (index < a.Length)

invariant 0 <= index;

invariant forall k :: 0 <= k < index && k < a.Length ==> a[k] != 0;

{

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

index := index + a[index];

}

index := -1;

This code will compute the right result, but Dafny complains about the second loop invariant. Dafny is not convinced that skipping all those elements is justified. The reason is that the pre-condition says that each successive element decreases by at most one, but it does not say anything about how elements further away are related. To convince it of this fact, we need to use a lemma.

Lemmas

The first and most common type of lemma is a method lemma. A method lemma is a method which has the desired property as a postcondition. The method does not change any state, and doesn't need to be called at runtime. For this reason, it is declared to be a ghost method. It is present solely for its effect on the verification of the program. Method lemmas are kind of like heavyweight assertions, in that they are only necessary to help the proof of the program along. A typical method lemma might look like:

ghost method Lemma(...)

ensures (desirable property);

{

...

}

For the zero search problem, the desirable property is that none of the elements from index untilindex + a[index] can be zero. We take the array and the index to start from as parameters, with the usual requirements from FindZero:

edit

ghost method SkippingLemma(a : array<int>, j : int)

requires a != null;

requires forall i :: 0 <= i < a.Length ==> 0 <= a[i];

requires forall i :: 0 < i < a.Length ==> a[i-1]-1 <= a[i];

requires 0 <= j < a.Length;

ensures forall i :: j <= i < j + a[j] && i < a.Length ==> a[i] != 0;

{

...

}

The postcondition is just the desirable property that we want. The extra restriction on i is because j + a[j] could be past the end of the array. We only want to talk about indices in that range which are also indices into the array. We then do a crucial step: check that our lemma is sufficient to prove the loop invariant. By making this check before filling in the lemma body, we ensure that we are trying to prove the right thing. The FindZero method becomes:

edit

index := 0;

while (index < a.Length)

invariant 0 <= index;

invariant forall k :: 0 <= k < index && k < a.Length ==> a[k] != 0;

{

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

SkippingLemma(a, index);

index := index + a[index];

}

index := -1;

Now Dafny does not complain about the FindZero method, as the lemma's postcondition shows that the loop invariant is preserved. It does complain about the lemma itself, which is not suprising given that the body is empty. In order to get Dafny to accept the lemma, we will have to demonstrate that the post-condition is true. We do this like we do everything in Dafny: writing code.

We start with the crucial property of the array, that it only decreases slowly. We can ask whether certain properties hold by using assertions. For example, we can see that Dafny knows:

edit

assert a[j ] - 1 <= a[j+1];

assert a[j+1] - 1 <= a[j+2];

assert a[j+2] - 1 <= a[j+3];

// therefore:

assert a[j ] - 3 <= a[j+3];

Thus we can see that Dafny can follow along in any individual step, and can even chain them appropriately. But the number of steps we need to make is not constant: it can depend on the value of a[j]. But we already have a construct for dealing with a variable number of steps: the while loop!

We can use the very same construct here to get Dafny to chain the steps together. We want to iterate from j to j + a[j], keeping track of the lower bound as we go. We also keep track of the fact that all of the elements we have seen so far are not zero:

edit

var i := j;

while(i < j + a[j] && i < a.Length)

invariant i < a.Length ==> a[j] - (i-j) <= a[i];

invariant forall k :: j <= k < i && k < a.Length ==> a[k] != 0;

{

i := i + 1;

}

The first invariant gives the bound on the current element, if we haven't run into the end of the array already. For each index past j (of which there are i-j), the array can be one smaller, so this value is subtracted from a[j]. This only says that the current element cannot be zero, so without the second invariant, Dafny would not be able to know that there were no zeros. Dafny forgets everything about the executions of the loop except what is given in the invaraints, so we need to build up the fact that there were no zeros anywhere so far.

That's it! The body of the loop just increments the counter. As we saw before, Dafny is able to figure out each step on its own, so we don't need to do anything further. We just needed to give it the structure of the proof it needed to make. Sometimes the individual steps themselves are complex enough that they need their own little subproofs, using either a series of assert statements or a whole other lemma.

When working with arrays, iteration is a natural solution to many problems. There are some times, however, when recursion is used to define functions or properties. In these cases, the lemmas usually have the same recursive structure. To see an example of this, we will consider the problem of counting.

Counting

We will count the number of trues in a sequence of bools, using the count function, given below:

edit

function count(a: seq<bool>): nat

{

if |a| == 0 then 0 else

((if a[0] then 1 else 0) + count(a[1..]))

}

...

assert count([]) == 0;

assert count([true]) == 1;

assert count([false]) == 0;

assert count([true, true]) == 2;

...

The code is very straightforward, but one thing to notice is that the function is defined recursively. Recursive functions like this are prone to requiring lemmas. There is a desirable property of count that we would like to be able to use in verifying a program that uses this function: it distributes over addition. By this we mean:

forall a, b :: count(a + b) == count(a) + count(b)

Here, the first plus (+) is sequence concatenation, and the second is integer addition. Clearly, we can break any sequence into two sequences a and b, count them seperately, and add the results. This is true, but Dafny cannot prove it directly. The problem is that the function does not split the sequence in this way. The function takes the first element, computes its count, then adds it to the rest of the sequence. If a is long, then in can be a while before this unrolling process actually reaches count(b), so Dafny does not attempt to unwrap more than a few recursive calls. (Two, to be exact. See the How Dafny Works tutorial for more information.) This is an example of a property that requires a lemma to demonstrate.

In our case, we have two options for the lemma: we could write the same universal quantifier we had above, or we could make the lemma specific to a pair of sequences a and b. It turns out that when we want the distributive property, we don't need the full universal property. We are just interested in the fact that count(a + b) == count(a) + count(b) for two specific a and b that are known in the program. Thus when we invoke the lemma to get the property, we can tell it which two sequences we are interested in. If we have different sequences somewhere else, we can call the method with different arguments, just like a regular method. It turns out that proving the full universal property, while possible, is more work than proving the concrete, specific case, so we will tackle this case first.

Thus the lemma should take as arguments the sequences of interest, and the post-condition is as follows:

edit

ghost method DistributiveLemma(a: seq<int>, b: seq<int>)

ensures count(a + b) == count(a) + count(b);

{

}

Proving the Distributive Property

In order to write the lemma, we have to figure out a strategy for proving it. As you can verify above (no pun intended), the lemma does not work yet, as otherwise a lemma would be unnecessary. To do this, we note that the reason that Dafny could not prove this in the first place is that the count function is defined from the start of the sequence, while the distributive property operates on the middle of a sequence. Thus if we can find a way to work from the front of the sequence, then Dafny can follow along using the definition of the function directly.

Well, what is the first element of the sequence? There are a few cases, based on which (if any) ofa and b are the empty sequence. Thus our lemma will have to consider multiple cases, a common trait of lemmas. We notice that if a == [], then a + b == b, regardless of what b is. Lemmas handle cases using the same thing code does to handle cases: if statements. A short proof of the desirable property is given using asserts below.

edit

if (a == [])

{

assert a + b == b;

assert count(a) == 0;

assert count(a + b) == count(b);

assert count(a + b) == count(a) + count(b);

}

else

{

...

}

We can test our lemma in this case by adding a requires clause that restricts a to this case. We find that the code verifies. This means that if a == [], then our lemma will correctly prove the post-condition. In this case, only the first assertion above is necessary; Dafny gets the rest of the steps on its own (try it!). Now we can consider the other case, when 0 < |a|.

Our goal is to relate count(a + b) to count(a) and count(b). If a is not the empty sequence, then when we employ our trick of following the definition to expand count(a + b), we get:

edit

assert a + b == [a[0]] + (a[1..] + b);

assert count(a + b) == count([a[0]]) + count(a[1..] + b);

Notice that we get count([a[0]]) and a[1..]. These two terms would also appear if we expanded count(a). Specifically:

edit

assert count(a) == count([a[0]]) + count(a[1..]);

Finally, we can substitute this definition for count(a) into the post-condition to get:

assert count(a + b) == count(a) + count(b); // post-condition

assert count(a + b) == count([a[0]]) + count(a[1..]) + count(b);

Now this looks very similar to the expression we got after expanding count(a + b). The only difference is that count(a[1..] + b) has become count(a[1..]) + count(b). But this is exactly the property we are trying to prove!

Induction

The argument we are trying to make is inductive. We can prove our goal given that a smaller version of the problem is true. This is precisely the concept of induction: use a smaller version of a problem to prove a larger one. To do this, we call the recursive property from within our code. It is a method, so it can be invoked whenever we need it.

Dafny will assume that the recursive call satisfies the specification. This is the inductive hypothesis, that all recursive calls of the lemma are valid. This depends crucially on the fact that Dafny also proves termination. This means that eventually, the lemma won't make another recursive call. In this instance, this is the first branch of the if statement. If there is no recursive call, then the lemma must be proven directly for that case. Then each call in the stack is justified in assuming the lemma works for the smaller case. If Dafny did not prove the chain terminated, then the chain could continue forever, and the assumption for each call would not be justified.