Using Dafny, an Automatic Program Verier

Luke Herbert , K. Rustan M. Leino , and Jose Quaresma

1

Technical University of Denmark (lthhe,jncq)@imm.dtu.dk

2
Microsoft Research [email protected]

These lecture notes present Dafny, an automated program

verication system that is based on the concept of dynamic frames and
is capable of producing .NET executables. These notes overview the basic
design, Dafny's history, and summarizes the environment conguration.
The key language constructs, and various system limits, are illustrated
through the development of a simple Dafny program. Further examples,
linked to online demonstrations, illustrate Dafny's approach to loop invariants, termination, data abstraction, and heap-related specications.
Abstract.

Preface

These lecture notes introduce the programming and verication language Dafny.
They are primarily based on lectures given by Rustan Leino in 2011 at the 8th
LASER Summer School, as transcribed by Luke Herbert and Jose Quaresma
(who were students at that summer school). Other references to Dafny and
inuences on this tutorial include the Marktoberdorf Summer School lectures
from 2008 [11] and 2011 [10], and the online Dafny tutorial [9].
Dafny is a state-of-the-art implementation of an automated verication system based around the idea of dynamic frames [6,7]. This is an approach to
formal verication of program correctness that attempts to prove correctness
of individual program parts locally, and from there infer the correctness of the
whole program. The dynamic-frames approach makes it possible to reason about
subparts even in the presence of data-abstraction [15]. Dafny is a usable implementation of this approach which has been used to verify several non-trivial
algorithms.
This tutorial is a practical guide to using Dafny to write veriable programs.
While some description of the design of Dafny is given, this is not complete and
serves mostly to overview Dafny use, and to point to more authoritative sources
of information on Dafny internals.
This tutorial provides extensive code examples. Most code examples have web
links to code pre-loaded in an online Dafny environment, which demonstrates
many key Dafny features. You can follow the code examples by visiting the corresponding footnote link, to see what Dafny reports, and to further experiment
with Dafny.

Dafny Background

The Dafny programming language is designed to support static verication of

programs. It is imperative, sequential, supports generic classes and dynamic allocation, and, crucially, incorporates specication constructs. The specications
include pre- and post- conditions, frame specications (read and write sets), loop
invariants, and termination metrics. To further support specications, the language also oers updatable ghost variables, recursive functions, and types like
algebraic datatypes, sets, and sequences. Specications and ghost constructs are
used only during verication; the compiler omits them from the executable code.
The Dafny compiler produces C# code, which is in turn compiled to MSIL bytecode for the .NET platform by the standard Microsoft C# compiler. However,
the facilities for interfacing with other .NET code are minimal.
An overview of the entire Dafny system is given in gure 1. The Dafny verier is run as part of the compiler. A programmer interacts with it much in
the same way as with the static type checker; when the tool produces errors,
the programmer responds by changing the program's type declarations, specications, and statements. Dafny's program verier works by translating a given
Dafny program into the intermediate verication language Boogie 2 [1] in such
a way that the correctness of the Boogie program implies the correctness of the
Dafny program. Thus, the semantics of Dafny are dened in terms of Boogie
(a technique applied by many automatic program veriers). The Boogie tool is
then used to generate rst-order verication conditions that are passed to the Z3
SMT solver [4]. Any violations of these conditions are passed back as verication
errors. In parallel with the verication of the code, a standard .NET executable
is also emitted.

Fig. 1.

The Dafny system

Dafny is a descendant of a series of program veriers and extended static

checkers. When the Dafny project started, the most recent of these to reach some
maturity was the Spec# system [2], and a project to build the C program verier
VCC [3] was also in progress. Dafny started o as a research test bed for some
specication ideas that were being considered for VCC. Dafny provided a more
readable notation than the more primitive intermediate verication language
Boogie, on which both Dafny and VCC rest. Dafny showed itself to be useful in
verifying little algorithms. To handle more complicated algorithms, features were
gradually added to Dafny. Dafny has grown from a programming notation to a
full programming language, and from a language intended only for verication
to a language that also compiles to executable code. Dafny has been used to
verify a number of challenging algorithms, like the Schorr-Waite graph marking
algorithm [12] and Floyd's tortoise and hare cycle detection algorithm. Dafny
has also fared well in some program verication competitions [8]. Because the
language was designed from scratch and with verication in mind from the start,
it generally gives rise to cleaner programs than, say, programs veried with
VCC, whose specications are layered on top of an existing language. Moreover,
because Dafny is type safe and uses unbounded integers, specications written
in Dafny are typically simpler than what is seen in, for example, VCC. For these
reasons, Dafny stands out as a good choice for teaching concepts of program
reasoning.

Getting Started with Dafny

To get started, we suggest using the interactive version of Dafny on

rise4fun.com/Dafny.

http://

While this does not provide all the capabilities of the

full Visual Studio version of the tool, in particular with regard to debugging, it
is able to thoroughly demonstrate the main capabilities of Dafny. Indeed, this
entire tutorial can be completed using the

rise4fun

website.

http://
boogie.codeplex.com. The binaries run on any .NET platform, which includes
To run Dafny using your own computer, download the binaries from

Windows as well as any system with the Mono .NET development framework.
The smoothest way to run Dafny is in Microsoft Visual Studio 2010, which
brings the benets of an integrated development environment where the program
verier runs in the background as the Dafny code is being developed. The installation currently requires downloading and building Dafny from source (also from

http://boogie.codeplex.com) and dealing with some hardcoded le paths (see

the instructions on that site).
We also suggest you load the

rise4fun

website and type in the following

declaration of a simple method that swaps two variables.

method

Swap ( a

: int

: int ) returns

(x

: int

: int )

This method declaration states that the Swap method receives two values a
and b as input and returns two values x and y as output. The intention is to let

the output values be the input values in swapped order, that is to say that x
should have the value of b and y the value of a.
The central idea in Dafny is to express what the method is intended to do,
and then have Dafny verify that this is indeed what the method actually does
(an implementation of the concept of Hoare Logic [5]). Dafny can use an

ensures

declaration to express a postcondition for a method, informing Dafny that the

variables should be swapped after execution of the method. This is applied to
the example as follows:

method Swap ( a : i n t ,
e n s u r e s x == b &&

: int ) returns

(x

: int

: int )

y == a ;

After the signature of the method has been declared, we can write the body
of the method which implements the swapping and use Dafny to verify that the
method does indeed achieve what is intended. The suggested way to use Dafny
is to rst express what a method is intended to do, and then write the implementation of the method and let Dafny check if it is correct. For the preceding

example , try to see if you can write a satisfactory method body.

The Basics of the Dafny Language

The swap example from section 3 on the previous page can be used to introduce
the basic constructs of the Dafny language. That example used two of Dafny's
basic constructs, namely

method

and

ensures.

Here is a body of imperative code

for the method:

method Swap ( a : i n t ,
e n s u r e s x == b &&

: int ) returns

(x

: int

: int )

y == a ;

{
x
y

:=
:=

b;
a;

The method body is contained within the braces and it consists of a series of
statements, such as assignments, conditionals, loops, and method calls. Assignments in Dafny are performed using

:=

and simple statements are followed by a

semi-colon.
The types of parameters, result values, and object elds must be declared
explicitly, whereas the types of local variables (and of bound variables of quantied expressions, see section 7 on page 13) are usually inferred and can be

bool for booleans, int for unbounded integers,

nat for natural numbers (the non-negative integers, a subrange of int ). Userdened classes and inductive datatypes are allowed. Dafny provides set <T> for
an immutable nite set of values of type T, and seq<T> for an immutable nite
omitted. Dafny's types include
and

sequence of values of type T. In addition, there are array types of one and more

Interactive code sample: http://rise4fun.com/Dafny/VjhK

dimensions, written
type

object

array <T>, array2 <T>, array3 <T>,

and so on. Finally, the

is a super-type of all reference types, implying that a value of

can be a reference to any class instance or array, or the special value

null .

object
How-

ever, it should be noted that Dafny has no inheritance support or other class
subtypes.
The

ensures

keyword is used to specify a method's postcondition. A postcon-

dition expresses a property that must hold after every invocation of the method
through all possible return points. Postconditions form part of the method declaration and appear before the body block. In the Swap method, the postcondition
says that the output values should have the inverse order from the input arguments.
To make the example more interesting, instead of using method in- and outparameters, we can change the method to operate on two variables in the scope
enclosing the method. These variables are declared using the keyword

var outside

the scope of the method. To be able to verify this new version of the Swap method,
two important modications are needed.
The rst modication is due to the fact that the postcondition must be
expressed in terms of the state of the variables before and after method execution.
Dafny allows for this by making use of the

old

keyword, which when applied to

a variable ( old ( variable ) ) operates as a function which refers to the value of the
variable at the time the method was invoked.
The second modication required is to declare which variables the method
is allowed to change, which is done using the keyword

modies .

Although the

declared variables may look like global variables, they are in fact elds of an
implicit class. For now, just specify the Swap method with

modies this ,

which

gives the method license to modify the elds of the object on which it is invoked, which here means it is allowed to modify the variables x and y. These
modications result in a new swap program:

var
var

x
y

: int
: int

;
;

method Swap ( )
modifies this ;
e n s u r e s x == o l d ( y )

&& y ==

old ( x ) ;

{
x
y

:=
:=

y;
x;

If you attempt to verify this code, Dafny reports that a postcondition might
not hold. This is because the implementation of the method is now wrong. As
an exercise, try to implement it correctly.

One possible solution using a temporary variable will look like this :

var
4

tmp

:=

x;

Interactive code sample: http://rise4fun.com/Dafny/hpru

x
y

:=
:=

y;
tmp ;

The body of the Swap method can be expressed more succinctly by employing

parallel assignment. This avoids the use of a temporary variable and performs

the swap in a single line of code .

x ,y

:=

y ,x;

If a Dafny program contains a unique parameter-less method called Main, then

program execution will start there. It is not necessary to have a main method to
do verication, only to produce a .NET executable. We will now create a Main
method which will call our Swap method to perform a swap.
The main method sets the initial value for variables x and y, call the Swap
method, and then check if the values of the variables were indeed swapped. This
is conrmed by means of an assertion indicated by the

method Main ( )
modifies this

assert

keyword.

{
x
y

:=
:=

5;
10;

Swap ( ) ;

assert

x == 1 0 && y == 5 ;

An assertion statement forces Dafny to verify that the given boolean expression evaluates to true along all possible program paths to that point. You
can think of the program as crashing if the asserted condition does not hold.
Thus, only executions where the asserted condition holds ever get past the

assert
6

statement. You can observe a consequence of this in the following Warn method ,
where the verier complains about the rst

assert

statement but not the second

because the second assertion does hold in every execution that gets past the rst
assertion without crashing.

method
{

Warn ( )

var x ;
assert
assert

x <10;
x <100;

It is okay to think of

assert

as possibly crashing the program at run time,

but note that programs must pass the verier before they are compiled, and the
verier will complain if it cannot prove the absence of such crashes.

You can now verify the complete swap program . An alternative way to
implement the Swap method is:

5
6
7

Interactive code sample: http://rise4fun.com/Dafny/Zw5s

Interactive code sample: http://rise4fun.com/Dafny/AvCs
Interactive code sample: http://rise4fun.com/Dafny/slYEo

x
y
x

:=
:=
:=

x + y;
x
x

y;
y;

You can check that the Swap method making use of this alternative method

8 can also be veried by Dafny. Note that Dafny is able to reason

implementation

about the arithmetic performed. While Dafny is able to reason about many
common mathematical constructs that appear in programs, like linear arithmetic
and boolean algebra, Dafny is not aware of all mathematical truths. For example,
in the following program, which requires a complex mathematical proof [16],
Dafny will not be certain that the postcondition will always hold.

method F e r m a t ( a : i n t , b : i n t
e n s u r e s ( a n s == t r u e ) ;
{
ans

if

:= t r u e

: int ) returns

( ans

: bool )

( 0 < a && 0 < b && 0 < c && a * a * a + b * b * b == c * c * c )

ans

:= f a l s e

}
}

We can make the code more reusable if we change the swap program to use
an object encapsulating the data instead of using global variables. We will create
a class called Cell in Dafny in the following way:

class
var

Cell
data

: int

We created a class Cell with one integer variable called

data.

We can now

change the signature of the Swap method to make use of Cell objects. This
new version of the method will receive two Cell objects and swap their values.
However, this introduces a new requirement that the method's input parameters
should refer to proper Cell objects, that is, they can not have the

null

value.

We express this requirement using a precondition, a boolean expression which is

declared using the

requires

keyword. It is the responsibility of the caller to make

sure the preconditions hold at the call site, and it is the responsibility of the
callee (i.e. the method body) to make sure that the postconditions hold upon
return from the method.
Using the Cell class, we now have the following Swap method, which includes
pre- and post- conditions:

method Swap ( x : C e l l , y : C e l l )
r e q u i r e s x != n u l l && y != n u l l ;
e n s u r e s x . d a t a == o l d ( y . d a t a ) &&

y . d a t a ==

old ( x . data ) ;

8
9

Interactive code sample: http://rise4fun.com/Dafny/OUQP

Interactive code sample: http://rise4fun.com/Dafny/iwHS

x . data
y . data
x . data

:=
:=
:=

x . data + y . data ;
x . data
x . data

y . data ;
y . data ;

To accommodate the new Cell class, we will also update the method that
calls the Swap method:

method
{

var

Main ( )
c ,

c . data
Swap ( c ,

assert
assert

:= new

:=

10;

Cell ,
d . data

new
:=

Cell ;
20;

d);
d . d a t a == 1 0 ;
c . d a t a == 2 0 ;

In this version of the swap program

10 , Dafny will report a new error. Namely

that the Swap method performs an assignment which may update an object not
in the enclosing context's modies clause. This is due to the fact that, while
methods are allowed to read whatever memory they like, they are required to
declare which parts of memory they modify. The declaration is done with a

modies

annotation, which lists the objects (or sets of objects) whose elds may

be modied. In this case, the method changes the elds of the objects x and y,
so we change our method declaration to look like this:

method Swap ( x : C e l l , y : C e l l )
r e q u i r e s x != n u l l && y != n u l l ;
modifies x , y ;
e n s u r e s x . d a t a == o l d ( y . d a t a ) &&

y . d a t a ==

old ( x . data ) ;

{
x . data
y . data
x . data

:=
:=
:=

x . data + y . data ;
x . data
x . data

y . data ;
y . data ;

That will solve the issue with modifying the cells

11 . Dafny now reports that

the postcondition of our Swap method might not hold. This might be unexpected,
since almost the same code for the Swap method was veried earlier. The only
dierence is that we are now using instances of the Cell class. This is the source of
the problemthe variables dened in the Cell classes are referenced by pointers,
which means the program now behaves dierently. Specically, when x . data and
y . data refer to the same object, i.e., when the references x and y are the same,

the value of this data eld will always be 0 after we execute the Swap method.
To see if our reasoning is correct, we can use an assumption. An assumption
is a boolean expression, denoted by the

10
11

assume

keyword, which from that point

Interactive code sample: http://rise4fun.com/Dafny/lAKHt

Interactive code sample: http://rise4fun.com/Dafny/rG8

onward is treated as a verication axiom. When using an assumption, the verier

only considers execution paths where the control ow either does not reach that
assumption, or reaches the assumption and nds that its condition evaluates to
true. Assumption statements are helpful to use temporarily when debugging a
verication attempt, but they cannot be compiled and should not be left in the
nal program (the compiler will complain if they are).
Placing the assumption

assume

x != y; in the body of our erroneous Swap

method implementation causes it to verify, thus conrming our understanding

that the body is correct in this case

12 . The assumption has done its job, so let's

remove it and think about how to proceed.

One of the key benets of Dafny is now clear. The Dafny verication errors
produced while writing the Swap method show some of the subtle properties
of dierent implementations. In fact, Dafny has exposed a problem that will
lead to a key design choice. One option is to keep the current implementation
which is able to swap any two dierent cells, but which will return cells with
value

0 when asked to swap the same variable. This option requires changing the

specication, either by altering the postcondition

13 or by adding a precondition

14
that requires x and y to refer to dierent objects . Another option is to change
15
the implementation to allow for swapping without restrictions .

Loop Invariants

So far, the code examples we have used have consisted of a nite number of
control paths. When recursion or loops are involved, the number of control paths
may be innite. To reason about such control paths, it is necessary to provide
annotations at various program points along the way. For recursive calls, you
supply pre- and post- conditions, as we have already seen. For loops, you supply
a loop invariant.
A loop invariant is a boolean expression that holds at the start of every
iteration. The verier checks that the loop invariant holds at the point where
control ow reaches the loop and checks that it holds again at the end of every
loop iteration. Thereby, it can assume the loop invariant to hold at the very
top of each iteration (meaning at the point where the loop guard is about to be
evaluated), which is how the verier reasons about the code in the loop body
and after the loop. In fact, the loop invariant is the only property the verier
remembers about the variables being modied in the loop from one iteration to
another, so it is important to declare a loop invariant that says enough about
these variables. This is similar to the way calls are handled, where pre- and
post- conditions are the only properties that the verier takes across the call
boundaries.

12
13
14
15

Interactive
Interactive
Interactive
Interactive

code
code
code
code

sample:
sample:
sample:
sample:

http://rise4fun.com/Dafny/B78X
http://rise4fun.com/Dafny/YWYs
http://rise4fun.com/Dafny/HIBe
http://rise4fun.com/Dafny/6OL

To demonstrate the use of loop invariants, we will use a function. In Dafny, a

function body has exactly one expression, whose type corresponds to the function return type. These constructs can only be used in annotations and their
utility comes from the fact that they can be used to directly express program
specications. However, functions are not part of the compiled code; they are
just used to aid program verication.
Let's start by creating a recursive Fibonacci function that returns the value
of the n'th number of the zero-indexed Fibonacci sequence:

function
{

if

Fib (n

: nat ) : nat

then

n < 2

else

F i b ( n 2) + F i b ( n 1)

We can use this function in the loop invariant of an iterative version of the
Fibonacci method, and by making use of this invariant, Dafny can reason about
the loop in this method. This method will have the following signature:

method C o m p u t e F i b ( n : nat ) r e t u r n s
e n s u r e s x == F i b ( n ) ;

(x

: nat )

The method receives a natural number (n) as input, and returns a natural
number (x) which is the n'th Fibonacci number. The second line is the postcondition of the method and it tells us that the returned value is indeed the n'th
number of the zero indexed Fibonacci sequence.
In the body of the method, we wish to build the required Fibonacci number
iteratively. This can be done by using parallel assignment to both compute the
next Fibonacci number and perform the needed housekeeping of the position in
the sequence, in eect updating two numbers of the sequence at once. We will
use x and y to keep track of those two consecutive numbers, with y corresponding
to the newly computed number and x corresponding to number computed in the
previous iteration. That is to say, after i iterations of the loop, x is the i 'th
number of the Fibonacci sequence and y is the i +1'th.

method C o m p u t e F i b ( n : nat ) r e t u r n s
e n s u r e s x == F i b ( n ) ;
{

var
x

:=

:=

(x

: nat )

0;

0;

v a r y :=
while ( i

1;
< n)

{
x ,
i

:=

:=
i

y ,

x+y ;

1;

}
}

16 .

You can now see what Dafny what reports

16

Interactive code sample: http://rise4fun.com/Dafny/xeo

As you might expect, Dafny cannot be certain that the postcondition holds.
That is because there is no loop invariant that describes the values of x, y, and
i through the iterations. Let us supply a loop invariant. We begin by describing

the possible values of the loop index i . We know that i starts at 0, and it will
increase until it is equal to n at which point the program will exit the loop. So
this is the rst invariant:

invariant

0 <=

i <= n ;

We also need to describe x and y in the loop invariant, but for instructional
purposes, let's explore what happens if we mention just x and not y. Remember,
we intend the code to maintain x as the i 'th value of the Fibonacci sequence,
where i is the number of iterations performed. So, we write the following loop
invariant:

invariant

x == F i b ( i ) ;

Dafny can now tell that the postcondition will hold: Starting from the very
top of a loop iteration, the invariants about i and x hold. If the loop guard
( i < n) happens not to hold, that is, if n <= i, then the rst loop invariant
lets the verier conclude i == n and the second loop invariant lets the verier
conclude x == Fib(n), which is the desired postcondition.
However, Dafny will now tell us that the second loop invariant might not
be preserved by the loop. This is because the next value of x depends on the
previous value of y, about which our loop invariants do not yet say anything. So,
we need to provide some information about the value of y in the loop. Remember
our intention about y, which is to maintain it as the i +1'th Fibonacci number.
Adding the corresponding loop invariant and running Dafny will now report that
the program is veried successfully

function
{

if

Fib (n

n < 2

17 .

: nat ) : nat

then

else

F i b ( n 2) + F i b ( n 1)

method C o m p u t e F i b ( n : nat ) r e t u r n s
e n s u r e s x == F i b ( n ) ;
{

var
x

:=

:=

(x

: nat )

0;

0;

v a r y := 1 ;
while ( i < n)
invariant 0
invariant x
invariant y

<=

i <= n ;

== F i b ( i ) ;
== F i b ( i + 1 ) ;

{
x ,

17

:=

y ,

x+y ;

Interactive code sample: http://rise4fun.com/Dafny/l4ey

:=

1;

}
}

Looking back at what we just did, you may see striking similarities between
loop invariants and mathematical proofs that use induction. At any time, the
loop invariant says what is true after all the loop iterations so far. When no
loop iterations have taken place, you need to check that the loop invariant holds
initially, which corresponds to the base case in typical proofs by induction. To
prove that the loop invariant holds after
gets to assume that it holds after

k + 1 iterations (for an arbitrary k ), one

iterations, which corresponds to assuming

the inductive hypothesis when doing the inductive step in typical proofs by
induction.
So now we know that if we exit the loop in our ComputeFib method, the
postcondition will hold. But what if we don't exit the loop? It's clearly desirable
to have Dafny assure us that the program will denitely exit the loop.

Termination: Variant Functions

Dafny can prove termination by using decreases annotations. If we can label each
loop iteration with a natural number and make sure that successive iterations
strictly decrease that label, then it follows that at run time the program can
only execute a nite number of loop iterations, and that is all the information
needed to prove that the loop eventually terminates.
More generally, instead of a natural number, we can use any value as long
as we choose a well-founded relation which induces strictly decreasing chains,
i.e. it does not admit innite descending chains. Dafny predenes a well-founded
relation on each of its types, and it extends these to lexicographically ordered
tuples, which then also form a well-founded relation. The tuple of expressions
that labels a loop iteration is called a variant and is introduced using the keyword

decreases.

In the majority of cases, Dafny is able to infer the correct decreases

annotations, but sometimes these have to be made explicit by the programmer.

Usually, there is a loop variable that is being increased or decreased to control
the number of iterations. When the loop condition is an inequality, it is normally
the distance between the two variables that is decreasing. That is what happens
in the Fibonacci sequence example, where we have i < n as the loop condition
where

while

( i < n). In this case, Dafny infers that what decreases in the loop is

the dierence between n and i .

Similarly, innite recursion is avoided by labelling each recursive or mutually
recursive method or function with a variant, also introduced with the keyword

decreases.
Let us start by looking at an example of a simple recursive function that

18 . The decreases

returns the sum of all the elements of a sequence of integers

clause in the following example allows Sum to be calling itself with a sequence

18

Interactive code sample: http://rise4fun.com/Dafny/PAl

whose length is decreased by one at each invocation. Since there is a lower bound
on the size of a sequence, this implies ordering on successive calls is well-founded,
and thus the recursion will eventually terminate.

f u n c t i o n Sum ( x s : seq < i n t >) : i n t

decreases xs ;
{

if

x s ==

[]

then

else

xs [ 0 ]

+ Sum ( x s [ 1 . . ] )

19 . As you

Now consider a more complex example, the Ackermann function

can see, the decreases clause has the lexicographic tuple m,n that allows Dafny
to prove termination. It proves this by using size comparisons of the component
values to determine whether the measure has shrunk. In this case it uses two
integers, but in general each component can be of dierent types. The comparison
works lexicographically: if the rst element, in this case m, is smaller, then it
doesn't matter what happens to the other values. They could increase, decrease,
or stay the same. The second element is only considered if the rst element does
not change. Then, the second value needs to decrease. If it doesn't, then the third
element must decrease, etc. For proof of termination to be possible eventually,
one of the elements must decrease, and the values of any subsequent elements
are not taken into consideration.

f u n c t i o n A c k e r m a n n (m : nat ,
d e c r e a s e s m, n ;
{

if

m == 0

: nat ) : nat

then

n + 1

else i f

n == 0

then

A c k e r m a n n (m

1,

1)

A c k e r m a n n (m

1,

A c k e r m a n n (m,

else

1))

Looking more closely at the Ackermann function, there are three recursive
calls. In the rst, m becomes one smaller, but n increases. This makes the decreases clause valid since the rst element of the tuple decreases (and it doesn't
matter what happens to the ones after that). In the second call, m also decreases,
so the second argument is again allowed to be any value. Dafny then needs to
prove that the third call obeys the termination measure. For this call, m remains
the same, but n decreases, so the overall measure decreases as well. Dafny is thus
able to prove the termination of the Ackermann function.

Lemmas

Sometimes, intricate logical steps are required to prove program correctness, but
they are too complex for Dafny to discover and use on its own. An example of

19

Interactive code sample: http://rise4fun.com/Dafny/hUYe

this is the Fermat method shown in section 4 on page 7. When this happens, we
can often give Dafny assistance by providing a lemma, which is a theorem used
to prove another result.
Lemmas allow Dafny to break a proof into two: prove the lemma, then use
it to prove the nal result, i.e. the correctness of the program. Splitting up the
proof in this way helps Dafny to see the intermediate steps that make the proof
process easier. Lemmas are particularly useful for inductive arguments, which
are some of the hardest problems for theorem provers.
The 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 run time. For this reason, it is
declared to be a

ghost method. It is present solely for its eect on the verication

of the program, and to help the proof of the program. A typical method lemma
has the following structure:

g h o s t method Lemma ( . . . )
ensures ( d e s i r a b l e property ) ;
{
...
}

Consider the following example; we will write a method that receives an

array of integers as input and returns the index of the rst zero that occurs in
the array, or

if there are no zeros in the array. This is represented by the

following two postconditions:

e n s u r e s i n d e x < 0 ==>
( forall
i : : 0 <= i
e n s u r e s 0 <= i n d e x ==>

< a . L e n g t h ==> a [ i ]

i n d e x < a . L e n g t h && a [ i n d e x ]
(

forall

::

0 <=

<

!=

0);

== 0 &&

i n d e x ==> a [ i ]

!=

0);

Let's say that the array our method receives has two properties: its elements
are non-negative and its values cannot decrease by more than one unit in consecutive positions. We will add these properties as preconditions to our method:

requires forall
requires forall

i
i

::
::

0 <=
0 <

i
i

< a . L e n g t h ==> 0 <= a [ i ] ;

< a . L e n g t h ==> a [ i

1] 1

<= a [ i ] ;

When writing the method, we can take advantage of this property, because
if we know, for example, a [ j ] == 3, then we know that we will not nd a zero
before a [ j +3]. Generalizing this, if a [ j ] is non-zero, we know we will not nd a
zero before a [ j +a[j ]] (due to the property that successive array values decrease
by at most one) and, therefore, we can accordingly jump positions in the array

20 .

while looking for the zeros. We thus have our FindZero method

method F i n d Z e r o ( a : a r r a y < i n t >) r e t u r n s

r e q u i r e s a != n u l l ;
20

( index

: int )

Interactive code sample: http://rise4fun.com/Dafny/FVFT

r e q u i r e s f o r a l l i : : 0 <= i < a . L e n g t h ==> 0 <= a [ i ] ;

r e q u i r e s f o r a l l i : : 0 < i < a . L e n g t h ==> a [ i 1] 1 <= a [ i ] ;
e n s u r e s i n d e x < 0 ==>
( forall
i : : 0 <= i < a . L e n g t h ==> a [ i ] != 0 ) ;
e n s u r e s 0 <= i n d e x ==> ( i n d e x < a . L e n g t h && a [ i n d e x ] == 0 &&
( forall
i : : 0 <= i < i n d e x ==> a [ i ] != 0 ) ) ;
{
index

:=

0;

w h i l e ( i n d e x < a . Length )
i n v a r i a n t 0 <= i n d e x ;
invariant forall k : : 0
a[k]

if

!=

(a [ index ]

index

:=

<= k <

i n d e x && k < a . L e n g t h ==>

0;
== 0 )

index

return ;

+ a [ index ] ;

}
index

:= 1;

If you check this code using Dafny, it will report that it cannot prove the
loop invariant, since we are jumping several positions of the array. But we can
write a lemma that allows Dafny to prove that loop invariant.
We want to prove that the elements of the array between a [ j ] and a [ j +a[j ]]
cannot be zero. So we write a method that receives an array with the properties
mentioned previously and an index j and proves that there are no zeros between
a [ j ] and a [ j +a[j ]] .

g h o s t method JumpingLemma ( a : a r r a y < i n t > , j : i n t )

r e q u i r e s a != n u l l ;
r e q u i r e s f o r a l l i : : 0 <= i < a . L e n g t h ==> 0 <= a [ i ] ;
r e q u i r e s f o r a l l i : : 0 < i < a . L e n g t h ==> a [ i 1] 1 <=
r e q u i r e s 0 <= j < a . L e n g t h ;
e n s u r e s f o r a l l i : : j <= i < j + a [ j ] && i < a . L e n g t h
a[ i ]

!=

a[ i ];
==>

0;

{}

Before writing the body of this method, we can try to use it together with
the FindZero method to see if our lemma helps Dafny prove the loop invariant.
(It is not a problem that we didn't write the body yet, since when evaluating
the FindZero method, it will only use the postconditions from the JumpingLemma
method). The key change to the

21 :

while

loop in the FindZero method is shown

below

w h i l e ( i n d e x < a . Length )
i n v a r i a n t 0 <= i n d e x ;
invariant forall k : : 0
a[k]

!=

<= k <

i n d e x && k < a . L e n g t h ==>

0;

21

Interactive code sample: http://rise4fun.com/Dafny/7bN

if

(a [ index ]

== 0 )

return ;

JumpingLemma ( a , i n d e x ) ;
index

:=

index

+ a [ index ] ;

As you can see, Dafny is now able to prove the loop invariant in the FindZero
program. It still complains, but now because it is not able to prove the postcondition of our lemma, and it was not supposed to, since we didn't write the body
of the method yet.
When constructing the body, we want to iterate the array's index from j to
j + a[j ] (making sure that it is still smaller than the size of the array) and prove

that each of those elements is non-zero. The following code will achieve this:

v a r i := j ;
w h i l e ( i < j + a [ j ] && i < a . L e n g t h )
i n v a r i a n t i < a . L e n g t h ==> a [ j ] ( i j )
i n v a r i a n t f o r a l l k : : j <= k < i && k <
a[k]

!=

<= a [ i ] ;
a . L e n g t h ==>

0;

{
i

:=

1;

The rst invariant represents the fact that the value of a [ j ] subtracted by the
distance between j and i is smaller or equal than a [ i ] . This intuitively expresses
the fact that, for example, the value of a [ j +3] is not less than a [ j ]3. This
property can be inferred from the properties of the arrays, step by step. The
other invariant states that the values of the array between a [ j ] and a [ i ] (which
corresponds to the current iteration) are non-zero. Using this code as the method
body will allow Dafny to prove the postconditions of the lemma. In turn, the
postcondition of the lemma method allows the verier to prove that the loop
invariant in FindZero is maintained, which completes the proof of correctness of

22 .

FindZero

Note how the lemma and its proof were themselves expressed as a Dafny
method. Essentially, because Dafny already knows how to reason about calls
and loops, which are related to mathematical induction, these programming
features can also be used to prove lemmas by induction. This is powerful and
useful, and the power is accessible via ordinary constructs used in programming
and program verication.

Abstraction

So far, the programs we have seen would be considered examples of programming

in the small. For such programs, it is common that method specications serve
to hide the algorithmic details used in the method's implementation. When a
program is larger and contains reusable components, it is desirable to hide more

22

Interactive code sample: http://rise4fun.com/Dafny/bqu

implementation details than we have seen until now. In particular, it becomes

desirable to hide the details of how data is represented. That is the subject of
this section and the next.
To motivate and demonstrate abstraction in Dafny programs, let us introduce a class Counter, which behaves like a simple counter, with the following
specication:

class
{

var

Counter
Value

: int

constructor I n i t ()
modifies this ;
e n s u r e s V a l u e ==

0;

method G e t V a l u e ( ) r e t u r n s
e n s u r e s x == V a l u e ;

(x

: int )

method I n c ( )
modifies this ;
e n s u r e s V a l u e == o l d ( V a l u e )

1;

method Dec ( )
modifies this ;
e n s u r e s V a l u e == o l d ( V a l u e )

1;

We have not shown it here, but it is easy to write implementations for these

23 .

methods and to create a Main method to test the class and its specications

The variable Value is a simple way to explain the operation of the class to
clients. However, suppose the implementer of the class wants to represent Value in
an alternative way? To illustrate this point, suppose the Counter implementation
counts the number of increment and decrement operations; then Value can be
represented as the dierence between those two counts. We declare two more
variables:

var
var

incs
decs

: int
: int

;
;

These variables can be initialized in the constructor and updated appropriately

in the Inc and Dec methods.
We would now like to change the implementation of GetValue to compute the
return value in terms of incs and decs, rather than Value. That is, we want the
implementation to do x

:=

incs

decs, but we want the specication to still show

the postcondition as x == Value, which is simpler. To verify this postcondition,

it now becomes necessary to make explicit the relationship between the more abstract view of the class (Value) and the more concrete view of the implementation
( incs and decs).

23

Interactive code sample: http://rise4fun.com/Dafny/K9iD

One way to make this relationship explicit would be to add Value == incs

decs

to the postcondition of the constructor and to the pre- and post- conditions of
the methods. This would not be satisfactory, for two reasons. First, if the relation ever were to change, we would have to update the program text in many
places. Second, and more importantly, the details of this relation are to remain
private with the class implementation; clients of the class should not have to be
concerned with the details. So, we instead write the relation in the body of a
function that we shall name Valid :

function Valid () : bool

reads t h i s ;
{
V a l u e ==

incs

decs

In this declaration, we see a new annotation:

reads.

Just like methods have

to declare which parts of the object store they may update, functions have to
declare which parts of the object store they depend on. We will have more to
say about these so-called frame issues in the next section.
Finally, we need to use and enforce this relationship, which we do by adding
Valid () as postcondition of the constructor and as a pre- and post- condition of

all methods which ensures that if the relationship holds before invocation it must
also do so after execution. Since we now no longer need Value in the compiled
code, we can mark it as ghost.
By applying the suggested changes, we can now verify the program

24 . Because

Value is a ghost variable, it will not be present in the compiled code and hence

it is necessary to have the GetValue method so that we can have access to the
actual value of the Counter instance we will be using.

class

Counter

// p u b l i c v a r i a b l e
ghost var Value : i n t
// p r i v a t e v a r i a b l e s
var i n c s : i n t ;
var decs : i n t ;

function Valid () : bool

reads t h i s ;
{
V a l u e ==

incs

decs

constructor I n i t ()
modifies this ;
ensures Valid ( ) ;
e n s u r e s V a l u e ==
24

0;

Interactive code sample: http://rise4fun.com/Dafny/or9

{
incs ,

decs ,

Value

:=

0,

0,

0;

method G e t V a l u e ( ) r e t u r n s
requires Valid ( ) ;
e n s u r e s x == V a l u e ;

(x

: int )

{
x

:=

incs

decs ;

method I n c ( )
requires Valid ( ) ;
modifies this ;
ensures Valid ( ) ;
e n s u r e s V a l u e == o l d ( V a l u e )

1;

{
incs ,

Value

:=

incs

+ 1,

Value +

1;

method Dec ( )
requires Valid ( ) ;
modifies this ;
ensures Valid ( ) ;
e n s u r e s V a l u e == o l d ( V a l u e )

1;

{
decs ,

Value

:=

decs + 1 ,

Value

1;

}
}

method
{

var

Main ( )
c

:= new

c . Inc ( ) ;

Counter . I n i t ( ) ;

c . Inc ( ) ;

c . Dec ( ) ;
c . Inc ( ) ;

assert

c . V a l u e == 2 ;

Dynamic Frames

In the previous section, we presented a way to specify the behavior of a class in

terms of a ghost variable. We related the value of the ghost variable to the values
of implementation variables in a function Valid , which we mentioned in method
pre- and post- conditions (essentially as a class invariant [14]). This specication
idiom also applies when a class implementation uses more complicated data
structures, except that we need to extend the idiom to better deal with framing,
that is,

reads

and

modies

clauses.

Let us continue with the Counter example from the previous section, but use
our previous Cell class, from section 4 on page 7, for the incs and decs variables
instead of integers:

var
var

incs
decs

:
:

Cell ;
Cell ;

We let the constructor initialize these elds by allocating new Cell objects:
incs ,

:= new

decs

i n c s . data ,

Cell ,

d e c s . data ,

new

Value

Cell ;

:=

0,

0,

0;

In the other methods, we replace incs and decs with incs . data and decs . data,
respectively. We apply that replacement in function Valid , too; in addition, we
need Valid to express that the two Cell references are non-null and distinct:
incs

!=

null

V a l u e ==

&& d e c s

i n c s . data

!=

null

&&

incs

!=

d e c s &&

decs . data

25 , we get complaints about violating

If we try to verify the resulting program

the declared framesfunction Valid is reading more than its

and methods Inc and Dec modify more than their

modies

reads

clause allows,

clauses allow. A quick

x to this problem is to change these three frame specications to also list the
object referenced by incs and decs

26 . This quick x is unsatisfactory, because it

exposes the implementation elds incs and decs in public specications. We need
a way to abstract over these elds in the specications.
A solution to this problem is dynamic frames [6,7]. In Dafny, a dynamic
frame is simply an expression that denotes a set of objects and that is used in

reads and modies

clauses. The frame is dynamic in the sense that the expression

may evaluate to dierent sets of objects, depending on the program state. We

will now describe the standard idiom for using dynamic frames in Dafny.
We start by introducing a variable Repr, which will stand for the set of objects in the object's representation. In the case of Counter, that set of objects
is { this , incs , decs}. The type of Repr is

set <object>,

and since the eld will be

used only in specications, not at run time, we declare it as

ghost var

Repr

: s e t <o b j e c t

ghost.

>;

We change the constructor to initialize Repr to the desired set, and we change
the frames of methods Inc and Dec to:

modifies

Repr ;

which says that the method is allowed to modify an object in the set Repr. More
precisely, this
object

modies

clause gives the method license to modify the elds of any

that, at the time the method is invoked, is in the set denoted by Repr.

Note that the frame for the constructor Init is still just

this . This is desirable

and is part of the standard idiom. First, at the time the constructor is called,

25
26

Interactive code sample: http://rise4fun.com/Dafny/H065

Interactive code sample: http://rise4fun.com/Dafny/dqu

the eld Repr has an unknown value, so it would not make sense to list it in the

modies clause. Second, the data elds to which

Init assigns belong to objects that

were created after Init was invoked, and Dafny allows any such newly allocated
objects to be modied, without any need to mention them in the

modies

Third, the only other modications performed by Init are to elds of

permitted by

modies this .

clause.

this ,

as

We have a few more things to address before we are done. If we tried to verify

27 , the verier would complain that methods

the program as it stands now

and Dec do not respect their frames, which are specied by

modies

Inc

Repr. The

reason for this is that the preconditions of these methods do not say anything
about the contents of Repr. To address this problem, we want to change the
denition of Valid to say something about Repr. So, let us change the denition
of Valid to this:

function Valid () : bool

r e a d s t h i s , Repr ;
{

this in
in

incs
incs

R e p r &&

null

R e p r && d e c s

!=

V a l u e ==

i n R e p r &&
i n R e p r &&

d e c s &&
i n c s . data

decs . data

We did several changes here. First, validity now implies that

Second, by convention, we exclude

null

this

is in Repr.

from Repr (this isn't strictly necessary,

but we strongly recommend itin our experience, the verication errors that

null in Repr may not make it evident that the problem

null and can therefore be confusing). Third, we list incs
contained in Repr. Fourth, since Repr does not contain null ,

can arise from allowing

is somehow related to
and decs as being

it follows that incs and decs are non-null, so we don't need to mention those
properties explicitly. Finally, we changed the

reads

clause, which requires some

this ?

Why doesn't just

further explanation.
Why does the frame of Valid explicitly list

reads

Repr

suce?
It may seem that

reads

Repr would suce, since we intend

this

to be included

in Repr. However, when checking that the body of Valid adheres to the reads
frame, the verier does not know anything about Repr. It may help to consider
how the body of Valid would be evaluated from an arbitrary state at run time.
The rst conjunct ( this

false or true . If it evaluates

false without evaluating the other conjuncts.
If it evaluates to true , then this in Repr holds. In either case, note that the
remaining conjuncts are evaluated only if this in Repr holds, which means that
reads Repr implies the elds of this can be read. But to read the rst conjunct
itself, which includes the eld this . Repr, the verier needs to know that this is
to

false ,

in

Repr) can evaluate to either

the function can return

allowed by the frame. To break this bootstrapping circularity, we simply list

both

27

this

and Repr in the

reads

clause.

Interactive code sample: http://rise4fun.com/Dafny/aAwn

By changing Valid as described above, our class veries

28 , but we're not quite

nished yet, because our postcondition specications are not strong enough to
be useful for clients. Consider some client code, like the Main method we used to
test the class in the previous section

method
{

var

29 :

Main ( )
c

:= new

c . Inc ( ) ;

Counter . I n i t ( ) ;

c . Inc ( ) ;

c . Dec ( ) ;
c . Inc ( ) ;

assert

c . V a l u e == 2 ;

This code gives rise to several frame violation errors. The problem is that the
postconditions of Init and the other methods do not say enough about the objects
in Repr. For example, the specications would allow a method to change incs to
point to a Cell object in use by another Counter object

30 :

method S h a r e M e ( c n t : C o u n t e r )
r e q u i r e s V a l i d ( ) && c n t != n u l l && c n t . V a l i d
m o d i f i e s Repr ;
e n s u r e s V a l i d ( ) && V a l u e == o l d ( V a l u e ) ;
{

if

( i n c s . d a t a == c n t . i n c s . d a t a )
i n c s . data

:=

();

cnt . i n c s . data ;

}
}

Calling this method could lead to two Counter objects sharing the same representation. Dafny allows such specications and implementations, which are
sometimes useful. The situation is ne, because the possibility of sharing does
not escape the verier. Indeed, this is why the verier complains about the Main
client above.
To correct the problem, we show the nal part of the standard dynamicsframe idiom in Dafny. To the constructor, we add the postcondition:

e n s u r e s f r e s h ( Repr

this

});

which says that, upon return from Init , all objects other than

this

in Repr are

ones that were allocated after Init was invoked. In other words, Init sets Repr
to some set of newly allocated objects, except it may also possibly contain

this .

This specication is abstract enough to not explicitly mention the private Counter
implementation, and yet strong enough to allow a client to follow up the call to
Init

by a call to a method (like Inc or Dec) declared with

modies

Reprafter

all, any object newly allocated in Init is also newly allocated in the caller, Main,

28
29
30

Interactive code sample: http://rise4fun.com/Dafny/MsRQ

Interactive code sample: http://rise4fun.com/Dafny/uT0k
Interactive code sample: http://rise4fun.com/Dafny/7RSR

so the caller is allowed to modify the objects that, upon return from Init , are
contained in Repr.
We add a similar postcondition to the mutating methods Inc or Dec:

e n s u r e s f r e s h ( Repr o l d ( Repr ) ) ;
This postcondition says that any objects added to Repr are newly allocated. The

31 :

program now veries

class
var

Cell
data

: int

class

Counter

// p u b l i c v a r i a b l e
ghost var Value : i n t ;
g h o s t v a r R e p r : s e t < o b j e c t >;
// p r i v a t e v a r i a b l e s
var i n c s : C e l l ;
var decs : C e l l ;

function Valid () : bool

r e a d s t h i s , Repr ;
{

this in
in

incs
incs

R e p r &&

null

R e p r && d e c s

!=

i n R e p r &&
i n R e p r &&

d e c s &&

V a l u e ==

i n c s . data

decs . data

constructor I n i t ()
modifies this ;
e n s u r e s V a l i d ( ) && f r e s h ( R e p r
e n s u r e s V a l u e == 0 ;
{
incs ,

decs

i n c s . data ,
Repr
Repr

:=
:=

:= new

Cell ,

d e c s . data ,

this };

Repr + { i n c s ,

new

Value

this

});

Cell ;

:=

0,

0,

0;

decs };

method G e t V a l u e ( ) r e t u r n s
requires Valid ( ) ;
e n s u r e s x == V a l u e ;

(x

: int )

{
x

:=

i n c s . data

decs . data ;

31

Interactive code sample: http://rise4fun.com/Dafny/fGVu

method I n c ( )
requires Valid ( ) ;
m o d i f i e s Repr ;
e n s u r e s V a l i d ( ) && f r e s h ( R e p r o l d ( R e p r ) ) ;
e n s u r e s V a l u e == o l d ( V a l u e ) + 1 ;
{
i n c s . data ,

Value

:=

i n c s . data + 1 ,

Value +

1;

method Dec ( )
requires Valid ( ) ;
m o d i f i e s Repr ;
e n s u r e s V a l i d ( ) && f r e s h ( R e p r o l d ( R e p r ) ) ;
e n s u r e s V a l u e == o l d ( V a l u e ) 1 ;
{
d e c s . data ,

Value

:=

decs . data + 1 ,

Value

1;

}
}

method
{

var

Main ( )
c

:= new

c . Inc ( ) ;

Counter . I n i t ( ) ;

c . Inc ( ) ;

c . Dec ( ) ;
c . Inc ( ) ;

assert

c . V a l u e == 2 ;

Our explanation of the standard dynamic-frames idiom may have been long,
but the idiom is simple to follow: First, declare the ghost variable Repr, and let
Valid describe the contents of Repr as we did above. Then, declare constructors

(like Init ) to include the following specication:

modifies this ;
ensures Valid ()

&&

f r e s h ( Repr

this

});

declare mutating methods (like Inc and Dec) to include the following specication:

requires Valid ( ) ;
m o d i f i e s Repr ;
e n s u r e s V a l i d ( ) && f r e s h ( R e p r o l d ( R e p r ) ) ;
and declare query methods (like GetValue) to include the following specication:

requires

Valid ( ) ;

These idiomatic specications may be verbose, but they lend themselves to

modular specications and can exibly be adapted to allow various forms of
sharing of data structures.

10

Conclusion

Dafny is a general-purpose specication language and verier. Through programmerprovided specications and other annotations, it makes possible the verication
of the functional correctness of a program. The symbol manipulation in the
proofs themselves is performed in a mostly automatic fashion, hidden from the
user of the tool.
In these lecture notes, we have introduced Dafny through a series of simple
examples. We have demonstrated a key strength of Dafny, namely abstraction
and dynamic frames, which allow us to scale to larger programs (for further
information on this see, for example, [13]). By learning and using Dafny, you can
construct programs that behave as specied. The concepts you learn also apply
when programming in other languages, even if you don't have a verication tool
and instead do the reasoning informally.

Acknowledgments
We are indebted to the reviewers, who gave a lot of themselves to take us through
various drafts of these lecture notes. Thank you!

References
1.

Barnett, M., Chang, B.-Y. E., DeLine, R., Jacobs, B., and Leino, K.

Boogie: A modular reusable verier for object-oriented programs. In Formal

Methods for Components and Objects: 4th International Symposium, FMCO 2005
R. M.

2.

(Sept. 2006), F. S. de Boer, M. M. Bonsangue, S. Graf, and W.-P. de Roever, Eds.,

vol. 4111 of Lecture Notes in Computer Science, Springer, pp. 364387.

Barnett, M., Fhndrich, M., Leino, K. R. M., Mller, P., Schulte, W.,
and Venter, H.

3.

4.
5.
6.

7.

Specication and verication: The Spec# experience. Commu-

nications of the ACM 54, 6 (June 2011), 8191.

Cohen, E., Dahlweid, M., Hillebrand, M. A., Leinenbach, D., Moskal,

M., Santen, T., Schulte, W., and Tobies, S. VCC: A practical system for verifying concurrent C. In Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics (Berlin, Heidelberg, Aug. 2009), S. Berghofer,
T. Nipkow, C. Urban, and M. Wenzel, Eds., vol. 5674 of Lecture Notes in Computer
Science, Springer-Verlag, pp. 2342.
de Moura, L., and Bjrner, N. Z3: An Ecient SMT Solver, vol. 4963 of
Lecture Notes in Computer Science. Springer Berlin, Berlin, Heidelberg, Apr. 2008,
ch. 24, pp. 337340.
Hoare, C. A. R. An axiomatic basis for computer programming. Communications
of the ACM 12, 10 (Oct. 1969), 576580.
Kassios, I. T. Dynamic frames: Support for framing, dependencies and sharing
without restrictions. In FM 2006: Formal Methods, 14th International Symposium
on Formal Methods (Aug. 2006), J. Misra, T. Nipkow, and E. Sekerinski, Eds.,
vol. 4085 of Lecture Notes in Computer Science, Springer, pp. 268283.
Kassios, I. T. The dynamic frames theory. Formal Aspects of Computing 23
(2011), 267288.

8.

Klebanov, V., Mller, P., Shankar, N., Leavens, G. T., Wstholz, V.,
Alkassar, E., Arthan, R., Bronish, D., Chapman, R., Cohen, E., Hillebrand, M., Jacobs, B., Leino, K. R. M., Monahan, R., Piessens, F., Polikarpova, N., Ridge, T., Smans, J., Tobies, S., Tuerk, T., Ulbrich, M.,

The 1st veried software competition: Experience report. In FM

2011: Formal Methods - 17th International Symposium on Formal Methods (June
2011), M. Butler and W. Schulte, Eds., vol. 6664 of Lecture Notes in Computer
Science, Springer, pp. 154168.

and Wei, B.

9.
10.
11.

12.

13.

14.
15.
16.

Koenig, J.

Dafny guide, 2011.

Getting started with Dafny: A guide. IOS

Press, 2012. Summer School Marktoberdorf 2011 lecture notes, to appear.
Leino, K. R. M. Specication and verication of object-oriented software. In Engineering Methods and Tools for Software Safety and Security, M. Broy, W. Sitou,
and T. Hoare, Eds., vol. 22 of NATO Science for Peace and Security Series D:
Information and Communication Security. IOS Press, 2009, pp. 231266. Summer
School Marktoberdorf 2008 lecture notes.
Leino, K. R. M. Dafny: An automatic program verier for functional correctness.
In Proceedings of the 16th international conference on Logic for programming, articial intelligence, and reasoning (Berlin, Heidelberg, Apr. 2010), E. M. Clarke
and A. Voronkov, Eds., vol. 6355 of Lecture Notes in Computer Science, SpringerVerlag, pp. 348370.
Leino, K. R. M., and Monahan, R. Dafny meets the verication benchmarks
challenge. In Veried Software: Theories, Tools, Experiments, Third International
Conference, VSTTE 2010 (Aug. 2010), G. T. Leavens, P. W. O'Hearn, and S. K.
Rajamani, Eds., vol. 6217 of Lecture Notes in Computer Science, Springer, pp. 112
126.
Meyer, B. Object-oriented Software Construction. Series in Computer Science.
Prentice-Hall International, 1988.
Koenig, J., and Leino, K. R. M.

Deductive verication of object-oriented software: dynamic frames,

dynamic logic and predicate abstraction. PhD thesis, Karlsruhe Institute of TechWei, B.

nology, 2011.
Wiles, A. Modular elliptic curves and Fermat's last theorem. The Annals of
Mathematics 141, 3 (May 1995), 443551.