Dafny - guide (Dafny - guide.docx)

Dafny - guide

other tutorials    close

Getting Started with Dafny: A Guide

1. Introduction

2. Methods

3. Pre- and Post-conditions

4. Assertions

5. Functions

6. Loop Invariants

7. Termination

8. Arrays

9. Quantifiers

10. Predicates

11. Framing

12. Binary Search

13. Conclusion

Be sure to follow along with the code examples by clicking the "edit" link in the corner. See what the tool says, try to fix programs on your own, and experiment!

Introduction

Dafny is a language that is designed to make it easy to write correct code. This means correct in the sense of not having any runtime errors, but also correct in actually doing what the programmer intended it to do. To accomplish this, Dafny relies on high-level annotations to reason about and prove correctness of code. The effect of a piece of code can be given abstractly, using a natural, high-level expression of the desired behavior, which is easier and less error prone to write. Dafny then generates a proof that the code matches the annotations (assuming they are correct, of course!). Dafny lifts the burden of writing bug-free code into that of writing bug-free annotations. This is often easier than writing the code, because annotations are shorter and more direct. For example, the following fragment of annotation in Dafny says that every element of the array is strictly positive:

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

This says that for all integers k that are indices into the array, the value at that index is greater than zero. By writing these annotations, one is confident that the code is correct. Further, the very act of writing the annotations can help one understand what the code is doing at a deeper level.

In addition to proving a correspondence to user supplied annotations, Dafny proves that there are no run time errors, such as index out of bounds, null dereferences, division by zero, etc. This guarantee is a powerful one, and is a strong case in and of itself for the use of Dafny and tools like it. Dafny also proves the termination of code, except in specially designated loops.

Let's get started writing some Dafny programs.

Methods

Dafny resembles a typical imperative programming language in many ways. There are methods, variables, types, loops, if statements, arrays, integers, and more. One of the basic units of any Dafny program is the method. A method is a piece of imperative, executable code. In other languages, they might be called procedures, or functions, but in Dafny the term "function" is reserved for a different concept that we will cover later. A method is declared in the following way:

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

{

...

}

This declares a method called "Abs" which takes a single integer parameter, called "x", and returns a single integer, called "y". Note that the types are required for each parameter and return value, and follow each name after a colon (:). Also, the return values are named, and there can be multiple return values, as in below:

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

{

...

}

The method body is the code contained within the braces, which until now has been cleverly represented as "..." (which is not Dafny syntax). The body consists of a series of statements, such as the familiar imperative assignments, if statements, loops, other method calls, return statements, etc. For example, the MultipleReturns method may be implemented as:

edit

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

{

more := x + y;

less := x - y;

// comments: are not strictly necessary.

}

Assignments do not use "=", but rather ":=". (In fact, as Dafny uses "==" for equality, there is no use of a single equals sign in Dafny expressions.) Simple statements must be followed by a semicolon, and whitespace and comments (// and /**/) are ignored. To return a value from a method, the value is assigned to one of the named return values sometime before a return statement. In fact, the return values act very much like local variables, and can be assigned to more than once. The input parameters, however, are read only. Return statements are used when one wants to return before reaching the end of the body block of the method. Return statements can be just the return keyword (where the current value of the out parameters are used), or they can take a list of values to return. There are also compound statements, such as if statements. If statements require parentheses around the boolean condition, and act as one would expect:

edit

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

{

if (x < 0)

{ return -x; }

else

{ return x; }

}

One caveat is that they always need braces around the branches, even if the branch only contains a single statement (compound or otherwise). Here the if statement checks whether x is less than zero, using the familiar comparison operator syntax, and returns the absolute value as appropriate. (Other comparison operators are <=, >, <=, != and ==, with the expected meaning. See the reference for more on operators.)

Pre- and Post-conditions

None of what we have seen so far has any specifications: the code could be written in virtually any imperative language (with appropriate considerations for multiple return values). The real power of Dafny comes from the ability to annotate these methods to specify their behavior. For example, one property that we observe with the Abs method is that the result is always greater than or equal to zero, regardless of the input. We could put this observation in a comment, but then we would have no way to know whether the method actually had this property. Further, if someone came along and changed the method, we wouldn't be guaranteed that the comment was changed to match. With annotations, we can have Dafny prove that the property we claim of the method is true. There are several ways to give annotations, but some of the most common, and most basic, are method pre- and post-conditions.

This property of the Abs method, that the result is always non-negative, is an example of a post-condition: it is something that is true after the method returns. Post-conditions, declared with theensures keyword, are given as part of the method's declaration, after the return values (if present) and before the method body. The keyword is followed by the boolean expression and a semicolon, which are both required. Like an if or while condition and most specifications, a post-condition is always a boolean expression: something that can be true or false. In the case of the Abs method, a reasonable post-condition is the following:

edit

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

ensures 0 <= y;

{

...

}

You can see here why return values are given names. This makes them easy to refer to in the post-condition of a method. When the expression is true, we say that the post-condition holds. The post-condition must hold for every invocation of the function, and for every possible return point (including the implicit one at the end of the function body). In this case, the only property we are expressing is that the return value is always at least zero.

Sometimes there are multiple properties that we would like to establish about our code. In this case, we have two options. We can either join the two conditions together with the boolean and operator (&&), or we can write multiple ensures specifications. The latter is basically the same as the former, but it seperates distinct properties. For example, the return value names from theMultipleReturns method might lead one to guess the following post-conditions:

edit

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

ensures less < x;

ensures x < more;

{

more := x + y;

less := x - y;

}

The post-condition can also be written:

edit

ensures less < x && x < more;

or even:

edit

ensures less < x < more;

because of the chaining comparison operator syntax in Dafny. (In general, most of the comparison operators can be chained, but only "in one direction", i.e. not mixing greater than and less than. See the reference for details.)

The first way of expressing the post-conditions separates the "less" part from the "more" part, which may be desirable. Another thing to note is that we have included one of the input parameters in the post-condition. This is useful because it allows us to relate the input and output of the method to one another (this works because input parameters are read only, and so are the same at the end as they were at the beginning).

Dafny actually rejects this program, claiming that the first post-condition does not hold (i.e. is not true). This means that Dafny wasn't able to prove that this annotation holds every time the method returns. In general, there are two main causes for Dafny verification errors: specifications that are inconsistent with the code, and situations where it is not "clever" enough to prove the required properties. Differentiating between these two possibilities can be a difficult task, but fortunately, Dafny and the Boogie/Z3 system on which it is based are pretty smart, and will prove matching code and specifications with a minimum of fuss.

In this situation, Dafny is correct in saying there is an error with the code. The key to the problem is that y is an integer, so it can be negative. If y is negative (or zero), then more can actually be smaller than or equal to x. Our method will not work as intended unless y is strictly larger than zero. This is precisely the idea of a pre-condition. A pre-condition is similar to a post-condition, except that it is something that must be true before a method is called. When you call a method, it is your job to establish (make true) the pre-conditions, something Dafny will enforce using a proof. Likewise, when you write a method, you get to assume the pre-conditions, but you must establish the post-conditions. The caller of the method then gets to assume that the post-conditions hold after the method returns.

Pre-conditions have their own keyword, requires. We can give the necessary precondition toMultipleReturns as below:

edit

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

requires 0 < y;

ensures less < x < more;

{

more := x + y;

less := x - y;

}

Like post-conditions, multiple pre-conditions can be written either with the boolean and operator (&&), or by multiple requires keywords. Traditionally, requires precede ensures in the source code, though this is not strictly necessary (although the order of the requires and ensures annotations with respect to others of the same type can sometimes matter, as we will see later). With the addition of this condition, Dafny now verifies the code as correct, because this assumption is all that is needed to guarantee the code in the method body is correct.

Not all methods necessarily have pre-conditions. For example, the Abs method we have already seen is defined for all integers, and so has no pre-conditions (other than the trivial requirement that its argument is an integer, which is enforced by the type system). Even though it has no need of pre-conditions, the Abs function as it stands now is not very useful. To investigate why, we need to make use of another kind of annotation, the assertion.

Assertions

Unlike pre- and post-conditions, an assertion is placed somewhere in the middle of a method. Like the previous two annotations, an assertion has a keyword, assert, followed by the boolean expression and a semicolon. An assertion says that a particular expression always holds when control reaches that part of the code. For example, the following is a trivial use of an assertion inside a dummy method:

edit

method Testing()

{

assert 2 < 3;

}

Dafny proves this method correct, as 2 is always less than 3. Asserts have several uses, but chief among them is checking whether your expectations of what is true at various points is actually true. You can use this to check basic arithmetical facts, as above, but they can also be used in more complex situations. Assertions are a powerful tool for debugging annotations, by checking what Dafny is able to prove about your code. For example, we can use it to investigate what Dafny knows about the Abs function.

To do this, we need one more concept: local variables. Local variables behave exactly as you would expect, except maybe for a few issues with shadowing. (See the reference for details.) Local variables are declared with the var keyword, and can optionally have type declarations. Unlike method parameters, where types are required, Dafny can infer the types of local variables in almost all situations. This is an example of an initialized, explicitly typed variable declaration:

edit

var x: int := 5;

The type annotation can be dropped in this case:

edit

var x := 5;

Multiple variables can be declared at once:

edit