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

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

Explicit type declarations only apply to the immediately preceding variable, so here the booldeclaration only applies to z, and not x or y, which are both inferred to be ints. We needed variables because we want to talk about the return value of the Abs method. We cannot put Abs inside a specification directly, as the method could change memory state, among other problems. So we capture the return value of a call to Abs as follows:

edit

// use definition of Abs() from before.

method Testing()

{

var v := Abs(3);

assert 0 <= v;

}

This is an example of a situation where we can ask Dafny what it knows about the values in the code, in this case v. We do this by adding assertions, like the one above. Every time Dafny encounters an assertion, it tries to prove that the condition holds for all executions of the code. In this example, there is only one control path through the method, and Dafny is able to prove the annotation easily because it is exactly the post-condition of the Abs method. Abs guarantees that the return value is non-negative, so it trivially follows that v, which is this value, is non-negative after the call to Abs.

But we know something stronger about the Abs method. In particular, for non-negative x, Abs(x) == x. Specifically, in the above program, the value of v is 3. If we try adding an assertion (or changing the existing one) to say:

edit

assert v == 3;

we find that Dafny cannot prove our assertion, and gives an error. The reason this happens is that Dafny "forgets" about the body of every method except the one it is currently working on. This simplifies Dafny's job tremendously, and is one of the reasons it is able to operate at reasonable speeds. It also helps us reason about our programs by breaking them apart and so we can analyze each method in isolation (given the annotations for the other methods). We don't care at all what happens inside each method when we call it, as long as it satisfies its annotations. This works because Dafny will prove that all the methods satisfy their annotations, and refuse to compile our code until they do.

For the Abs method, this means that the only thing Dafny knows in the Testing method about the value returned from Abs is what the post-conditions say about it, and nothing more. This means that Dafny won't know the nice property about Abs and non-negative integers unless we tell it by putting this in the post-condition of the Abs method. Another way to look at it is to consider the method annotations (along with the type of the parameters and return values) as fixing the behavior of the method. Everywhere the method is used, we assume that it is any one of the conceivable method(s) that satisfies the pre- and post-conditions. In the Abs case, we might have written:

edit

method Abs(x: int) returns (y: int)

ensures 0 <= y;

{

y := 0;

}

This method satisfies the post-conditions, but clearly the program fragment:

edit

var v := Abs(3);

assert v == 3;

would not be true in this case. Dafny is considering, in an abstract way, all methods with those annotations. The mathematical absolute value certainly is such a method, but so are all methods that return a positive constant, for example. We need stronger post-conditions to eliminate these other possibilities, and "fix" the method down to exactly the one we want. We can partially do this with the following:

edit

method Abs(x: int) returns (y: int)

ensures 0 <= y;

ensures 0 <= x ==> x == y;

{

// body as before

}

This expresses exactly the property we discussed before, that the absolute value is the same for non-negative integers. The second ensures is expressed via the implication operator, which basically says that the left hand side implies the right in the mathematical sense (it binds more weakly than boolean "and" and comparisons, so the above says 0 <= x implies x == y). The left and right sides must both be boolean expressions.

The post-condition says that after Abs is called, if the value of x was non-negative, then y is equal to x. One caveat of the implication is that it is still true if the left part (the antecedent) is false. So the second post-condition is trivially true when x is negative. In fact, the only thing that the annotations say when x is negative is that the result, y, is positive. But this is still not enough to fix the method, so we must add another post-condition, to make the following complete annotation covering all cases:

edit

method Abs(x: int) returns (y: int)

ensures 0 <= y;

ensures 0 <= x ==> x == y;

ensures x < 0 ==> y == -x;

{

// body as before

}

These annotations are enough to require that our method actually computes the absolute value ofx. These post-conditions are not the only way to express this property. For example, this is a different, and somewhat shorter, way of saying the same thing:

edit

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

In general, there can be many ways to write down a given property. Most of the time it doesn't matter which one you pick, but a good choice can make it easier to understand the stated property and verify that it is correct.

But we still have an issue: there seems to be a lot of duplication. The body of the method is reflected very closely in the annotations. While this is correct code, we want to eliminate this redundancy. As you might guess, Dafny provides a means of doing this: functions.

Functions

function abs(x: int): int

{

...

}

This declares a function called abs which takes a single integer, and returns an integer (the secondint). Unlike a method, which can have all sorts of statements in its body, a function body must consist of exactly one expression, with the correct type. Here our body must be an integer expression. In order to implement the absolute value function, we need to use an if expression. An if expression is like the ternary operator in other languages.

edit

function abs(x: int): int

{

if x < 0 then -x else x

}

Obviously, the condition must be a boolean expression, and the two branches must have the same type. You might wonder why anyone would bother with functions, if they are so limited compared to methods. The power of functions comes from the fact that they can be used directly in specifications. So we can write:

edit

assert abs(3) == 3;

In fact, not only can we write this statement directly without capturing to a local variable, we didn't even need to write all the post-conditions that we did with the method (though functions can and do have pre- and post-conditions in general). The limitations of functions are precisely what let Dafny do this. Unlike methods, Dafny does not forget the body of a function when considering other functions. So it can expand the definition of abs in the above assertion and determine that the result is actually 3.

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

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

edit

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:

edit

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:

edit

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 post-conditions, 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:

edit

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

edit

var i: int := 0;

while (i < n)

invariant 0 <= i;