Learn more

To become a user of Dafny, follow the Dafny tutorial (opens in new tab) online.

You can also see Dafny in action in some episodes of Verification Corner (opens in new tab).

To learn more about the features of Dafny, the Dafny Quick Reference may be for you.

The following paper presents the salient features of Dafny, along with the Schorr-Waite algorithm written in Dafny.  If you’re scientifically or technically inclined, this is the one to read and cite:

K. Rustan M. Leino.  Dafny: An Automatic Program Verifier for Functional Correctness.  In LPAR-16, volume 6355 of LNCS, pages 348-370.  Springer, 2010. [PDF (opens in new tab)] [slides from the conference presentation (opens in new tab)]

To dig deeper into the technology behind Dafny, the following lecture notes from the Marktoberdorf 2008 summer school describe the encoding of Dafny into Boogie 2:

K. Rustan M. Leino.  Specification and verification of object-oriented software.  In Engineering Methods and Tools for Software Safety and Security, volume 22 of NATO Science for Peace and Security Series D: Information and Communication Security, pages 231-266.  IOS Press, 2009. [PDF (opens in new tab)] [slides from the lectures (opens in new tab)]

Opens in a new tab

Dafny Quick Reference

This page illustrates many of the most common language features in Dafny.  In order to get you started more quickly, the descriptions here are simplified–this page is not the language reference.  For example, this pages does not go into modules, iterators, or refinement, which you won’t need until you write larger or more advanced programs in Dafny.

Programs

At the top level, a Dafny program (stored as a file with extension .dfy) is a set of declarations. The declarations introduce types, methods, and functions, where the order of introduction is irrelevant.  These user-defined types include classes and inductive datatypes.  The classes themselves also contain a set of declarations, introducing fields, methods, and functions.  If the program contains a parameter-less method called Main, then execution of the compiled program starts there, but it is not necessary to have a main method to do verification.

Comments start with // and go to the end of the line, or start with /* and end with */ and can be nested.

Fields

In a class, a field x of some type T is declared as:

var x: T

Unlike for local variables and bound variables, the type is required and will not be inferred. The field can be declared to be a ghost field by preceding the declaration with the keyword ghost. Dafny’s types include bool for booleans, int for mathematical (that is, unbounded) integers, string for strings, user-defined classes and inductive datatypes, set for a finite mathematical (immutable) set of T values (where T is a type), and seq for a mathematical (immutable) sequence of T values. In addition, there are array types (which are like predefined “class” types) of one and more dimensions, written array, array2, array3, …. The type object is a supertype of all class types, that is, an object denotes any reference, including null. Another useful type is nat, which denotes a subrange of int, namely the non-negative integers.

Methods

A method declaration (either at the top level or inside a class) has the form:

method M(a: A, b: B, c: C) returns (x: X, y: Y, z: Y)requires Premodifies Frameensures Postdecreases Rank{Body}

where a, b, c are the method’s in-parameters, x, y, z are the method’s out-parameters, Pre is a boolean expression denoting the method’s precondition, Frame denotes a set of objects whose fields may be updated by the method, Post is a boolean expression denoting the method’s postcondition, Rank is the method’s variant function, and Body is a statement that implements the method. Frame can be a list of expressions, each of which is a set of objects or a single object, the latter standing for the singleton set consisting of that one object. The method’s frame is the union of these sets, plus the set of objects allocated by the method body.  For example, if c and d are parameters of a class type C, then

modifies {c, d}

modifies {c} + {d}

modifies c, {d}

modifies c, d

all mean the same thing.

If omitted, the pre- and postconditions default to true and the frame defaults to the empty set. The variant function is a list of expressions, denoting the unending lexicographic tuple consisting of the given expressions followed implicitly by “top” elements. If omitted, Dafny will guess a variant function for the method, namely the lexicographic tuple that starts with the list of the method’s in-parameters.

A method can be declared as ghost by preceding the declaration with the keyword ghost. By default, a method in a class has an implicit receiver parameter, this. This parameter can be removed by preceding the method declaration with the keyword static. A static method M in a class C can be invoked by C.M(…).

In a class, a method can be declared to be a constructor method by replacing the keyword method with the keyword constructor. A constructor can only be called at the time an object is allocated (see object-creation examples below), and for a class that contains one or more constructors, object creation must be done in conjunction with a call to a constructor.  Ordinarily, a method has a name, of course, but a class is allowed to have one constructor without a name–an anonymous constructor–like this:

constructor (n: int)modifies this{Body}

Often, ghost methods are used as lemmas.  This can be made clearer in the program text by declaring the method with lemma instead of ghost method.

Here is an example method that takes 3 integers as in-parameters and returns these in 3 out-parameters in sorted order:

method Sort(a: int b: int, c: int) returns (x: int, y: int, z: int)ensures x <= y <= z && multiset{a, b, c} == multiset{x, y, z}{x, y, z := a, b, c;if z < y {y, z := z, y;}if y < x {x, y := y, x;}if z < y {y, z := z, y;}}

Functions

A function declaration (either at the top level or inside a class) has the form:

function F(a: A, b: B, c: C): Trequires Prereads Frameensures Postdecreases Rank{Body}

where a, b, c are the method’s parameters, T is the type of the function’s result, Pre is a boolean expression denoting the function’s precondition, Frame denotes a set of objects whose fields the function body may depend on, Post is a boolean expression denoting the function’s postcondition, Rank is the function’s variant function, and Body is an expression that defines the function. The precondition allows a function to be partial, that is, the precondition says when the function is defined (and Dafny will verify that every use of the function meets the precondition). The postcondition is usually not needed, since the body of the function gives the full definition. However, the postcondition can be a convenient place to declare properties of the function that may require an inductive proof to establish. For example:

function Factorial(n: int): intrequires 0 <= nensures 1 <= Factorial(n){if n == 0 then 1 else Factorial(n-1) * n}

says that the result of Factorial is always positive, which Dafny verifies inductively from the function body. To refer to the function’s result in the postcondition, use the function itself, as shown in the example.

By default, a function is ghost, and cannot be called from non-ghost code. To make it non-ghost, replace the keyword function with the two keywords function method.  A function that returns a boolean can be declared with the keyword predicate (and then eliding the colon and return type).

By default, a function in a class has an implicit receiver parameter, this. This parameter can be removed by preceding the function declaration with the keyword static. A static function F in a class C can be invoked by F.M(…). This can give a convenient way to declare a number of helper functions in a separate class.

Classes

A class is defined as follows:

class C {// member declarations go here}

where the members of the class (fields, methods, and functions) are defined (as described above) inside the curly braces.

Datatypes

An inductive datatype is a type whose values are created using a fixed set of constructors. A datatype Tree with constructors Leaf and Node is declared as follows:

datatype Tree = Leaf | Node(Tree, int, Tree)

The constructors are separated by vertical bars. Parameter-less constructors need not use parentheses, as is shown here for Leaf.

For each constructor Ct, the datatype implicitly declares a boolean member Ct?, which returns true for those values that have been constructed using Ct. For example, after the code snippet:

var t0 := Leaf;var t1 := Node(t0, 5, t0);

the expression t1.Node? evaluates to true and t0.Node? evaluates to false. Two datatype values are equal if they have been created using the same constructor and the same parameters to that constructor. Therefore, for parameter-less constructors like Leaf, t.Leaf? gives the same result as t == Leaf.

A constructor can optionally declare a destructor for any of its parameters, which is done by introducing a name for the parameter. For example, if Tree were declared as:

datatype Tree = Leaf | Node(left: Tree, data: int, right: Tree)

then t1.data == 5 and t1.left == t0 hold after the code snippet above.

Generics

Dafny supports type parameters.  That is, any class, inductive datatype, method, and function can have type parameters. These are declared in angle brackets after the name of what is being declared. For example:

class MyMultiset { /*…*/ }datatype Tree = Leaf | Node(Tree, T, Tree)method Find(key: T, collection: Tree) { /*…*/ }function IfThenElse(b: bool, x: T, y: T): T { /*…*/ }

Statements

Here are examples of the most common statements in Dafny.

var LocalVariables := ExprList;Lvalues := ExprList;assert BoolExpr;print ExprList;

if BoolExpr0 {Stmts0} else if BoolExpr1 {Stmts1} else {Stmts2}

while BoolExprinvariant Invmodifies Framedecreases Rank{Stmts}

match Expr {case Empty => Stmts0case Node(l, d, r) => Stmts1}

break;return;

The var statement introduces local variables (which are not allowed to shadow other variables declared inside the same set of most tightly enclosing curly braces). Each variable can optionally be followed by :T for any type T, which explicitly gives the preceding variable the type T (rather than being inferred). The ExprList with initial values is optional. To declare the variables as ghost variables, precede the declaration with the keyword ghost.

The assignment statement assigns each right-hand side in ExprList to the corresponding left-hand side in Lvalues. These assignments are performed in parallel (more to the point, all necessary reads occur before the writes), so the left-hand sides must denote distinct L-values. Each right-hand side can be an expression or an object creation of one of the following forms:

new Tnew T.Init(ExprList)new T(ExprList)new T[SizeExpr]new T[SizeExpr0, SizeExpr1]

The first form allocates an object of type T. The second form additionally invokes an initialization method or constructor on the newly allocated object. The third form shows how the syntax differs from the second form when the constructor called is anonymous.  The other forms show examples of array allocations, in particular a one- and a two-dimensional array of T values, respectively.

The entire right-hand side of an assignment can also be a method call, in which case the left-hand sides are the actual out-parameters (omitting the := if there are no out-parameters).

The assert statement claims that the given expression evaluates to true (which is checked by the verifier).

The print statement outputs to standard output the values of the given print expressions. Characters in strings can be escaped; for example, of interest for the print statement is that n denotes a newline character inside a string.

The if statement is the usual one. The example shows stringing together alternatives using else if. The else branch is optional, as usual.

The while statement is the usual loop, where the invariant declaration gives a loop invariant, the modifies clause restricts the modification frame of the loop, and the decreases clause introduces a variant function for the loop. By default, the loop invariant is true, the modification frame is the same as in the enclosing context (usually the modifies clause of the enclosing method), and the variant function is guessed from the loop guard.

The match statement evaluates the source Expr, an expression whose type is an inductive datatype, and then executes the case corresponding to which constructor was used to create the source datatype value, binding the constructor parameters to the given names.  If they are not needed to mark the end of the match statement, then the curly braces that surround the cases can be elided.

The break statement can be used to exit loops, and the return statement can be used to exit a method.

Expressions

The expressions in Dafny are quite similar to those in Java-like languages. Here are some noteworthy differences.

In addition to the short-circuiting boolean operators && (and) and || (or), Dafny has a short-circuiting implication operator ==> and an if-and-only-if operator <==>. As suggested by their widths, <==> has lower binding power than ==>, which in turn has lower binding power than && and ||.

Dafny comparison expressions can be chaining, which means that comparisons “in the same direction” can be strung together. For example,

0 <= i < j <= a.Length == N

has the same meaning as:

0 <= i && i < j && j <= a.Length && a.Length == N

Note that boolean equality can be expressed using both == and <==>. There are two differences between these. First, == has a higher binding power than <==>. Second, == is chaining while <==> is associative. That is, a == b == c is the same as a == b && b == c, whereas a <==> b <==> c is the same as a <==> (b <==> c), which is also the same as (a <==> b) <==> c.

Operations on integers are the usual ones, except that / (integer division) and % (integer modulo) follow the Euclidean definition, which means that % always results in a non-negative number. (Hence, when the first argument to / or % is negative, the result is different than what you get in C, Java, or C#, see http://en.wikipedia.org/wiki/Modulo_operation (opens in new tab).)

Dafny expressions include universal and existential quantifiers, which have the form:

forall x :: Expr

and likewise for exists, where x is a bound variable (which can be declared with an explicit type, as in x: T) and Expr is a boolean expression.

Operations on sets include + (union), * (intersection), and – (set difference), as well as the set comparison operators < (proper subset), <= (subset), their duals > and >=, and !! (disjointness). The expression x in S says that x is a member of set S, and x !in S is a convenient way of writing !(x in S). To make a set from some elements, enclose them in curly braces. For example, {x,y} is the set consisting of x and y (which is a singleton set if x == y), {x} is the singleton set containing x, and {} is the empty set.

Operations on sequences include + (concatenation) and the comparison operators < (proper prefix) and <= (prefix). Membership can be checked like for sets: x in S and x !in S. The length of a sequence S is denoted |S|, and the elements of such a sequence have indices from 0 to less than |S|. The expression S[j] denotes the element at index j of sequence S. The expression S[m..n], where 0 <= m <= n <= |S|, returns a sequence whose elements are the n-m elements of S starting at index m (that is, from S[m], S[m+1], … up to but not including S[n]). The expression S[m..] (often called “drop m”) is the same as S[m..|S|], that is, it returns the sequence whose elements are all but the first m elements of S. The expression S[..n] (often called “take n”) is the same as S[0..n], that is, it returns the sequence that consists of the first n elements of S. If j is a valid index into sequence S, then the expression S[j := x] is the sequence that is like S except that it has x at index j. Finally, to make a sequence from some elements, enclose them in square brackets. For example, [x,y] is the sequence consisting of the two elements x and y such that [x,y][0] == x and [x,y][1] == y, [x] is the singleton sequence whose only element is x, and [] is the empty sequence.

The if-then-else expression has the form:

if BoolExpr then Expr0 else Else1

where Expr0 and Expr1 are any expressions of the same type. Unlike the if statement, the if-then-else expression uses the then keyword, and must include an explicit else branch.

The match expression is analogous to the match statement and has the form:

match Expr {case Empty => Expr0case Node(l, d, r) => Expr1}

The curly braces can be used to mark the end of the match expression, but most commonly this is not needed and the curly braces can then be elided.

Opens in a new tab

Dafny was a popular tool among the teams at the VSTTE 2012 program verification competition (opens in new tab).  It was also used at the COST Verification Competition 2011 (opens in new tab), as part of the FoVeOOS conference.  And it was used in the VSComp 2010 (opens in new tab) competition at VSTTE 2010, from which a report (opens in new tab) was published:

Vladimir Klebanov, Peter Müller, Natarajan Shankar, Gary T. Leavens, Valentin Wüstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, and Benjamin Weiss.  The 1st Verified Software Competition: Experience Report.  In FM 2011: Formal Methods – 17th International Symposium on Formal Methods, volume 6664 of LNCS, pages 154-168.  Springer, 2011.  [PDF (opens in new tab)]

(which won Best Paper Award at FM 2011).  You can find Dafny solutions to the problem sets of these competitions under the Test directory of the Dafny sources (opens in new tab).

Dafny has also been used to solve various verification benchmark challenges.  At the Verified Software: Tools, Techniques, and Experiments (VSTTE 2008) conference, Weide et al. presented some verification benchmarks to facilitate the comparison between different specification languages and verifiers.  This paper describes Dafny programs for those benchmarks:

K. Rustan M. Leino and Rosemary Monahan.  Dafny meets the Verification Benchmarks Challenge.  In VSTTE 2010, volume 6217 of LNCS, pages 112-126.  Springer, 2010. [PDF (opens in new tab)]

Dafny has also been used to solve some of the VACID-0 verification benchmarks:

K. Rustan M. Leino and Michał Moskal.  VACID-0: Verification of Ample Correctness of Invariants of Data-structures, Edition 0.  Tools and Experiments workshop at VSTTE 2010. [PDF (opens in new tab)]

Opens in a new tab

Dafny is being used in teaching.  Here’s a partial list of universities that are or have been using Dafny in some capacity in lectures and class work:

• Caltech, Rajeev Joshi (CS 116 (opens in new tab))
• Lomonosov Moscow State University, Eugene Kornykhin
• Kansas State University, Torben Amtoft
• Imperial College London, Sophia Drossopoulou and Will Sonnex
• NUI Maynooth, Rosemary Monahan
• ETH Zurich, Peter Müller
• University of Washington, Ethan Jackson; Emina Torlak
• University of Iowa, Cesare Tinelli
• Koç University, Serdar Taşıran
• Rice University, Swarat Chaudhuri (COMP 507 (opens in new tab))
• UNSW, Carroll Morgan
• University of Toronto, Azadeh Farzan
• Princeton, Andrew Appel
• CMU, Jonathan Aldrich
• Chalmers Technical University, Moa Johansson
• Eindhoven Technical University, Kees Huizing
• Ohio State University, Bruce Weide
• Clemson University, Murali Sitaraman
• FCT Universidade Nova de Lisboa, Luis Caires
• University of the Basque Country, Paqui Lucio
• University of Southampton, Michael Butler
• University of Twente, Marieke Huisman
• Yale, Ruzica Piskac
• SUNY Stony Brook, Annie Liu
• University of Edinburgh, Ian Stark (APL14 (opens in new tab))
• Lübeck University of Applied Sciences, Andreas Schaefer
• UniBw München, Birgit Elbl and Lothar Schmitz
• IIT Madras, Ganesan Ramalingam
• Clarkson University, Christopher Lynch
• Tel Aviv University, Mooly Sagiv
• University of Utah, Zvonimir Rakamaric
• Memorial University, Theodore Norvell
• University of California, Santa Cruz, Cormac Flanagan
• Trinity College Dublin, Vasileios Koutavas
• Farhad Mehta, HSR Hochschule für Technik Rapperswil

and tutorials and summer schools:

• Summer School Marktoberdorf, 2008 and 2011
• LASER Summer School, 2011
• Summer School on Logic and Theorem-Proving in Programming Languages, Eugene, OR, 2008
• Tutorial, KTH, Stockholm, 2012
• Invited tutorial, VSTTE 2012
• Tutorial, HILT 2012
• Tutorial, ICSE 2013

If you are, or have been, teaching using Dafny, Rustan Leino (opens in new tab) would love to know of your experience. And if you want a mention on these lists, please let him know.

Opens in a new tab

• Try Dafny in your browser (opens in new tab)
• Download (opens in new tab)Dafny
• Contribute to Dafny source (opens in new tab)
• Dafny online tutorial (opens in new tab)

Opens in a new tab