Dafny Meets the Verification Benchmarks Challenge
K. Rustan M. Leino1 and Rosemary Monahan2
1 Microsoft Research, Redmond, WA, USA
leino@microsoft.com
2 National University of Ireland, Maynooth, Co.Kildare, Ireland
Rosemary.Monahan@nuim.ie
Abstract. A suite of verification benchmarks for software verification tools and
techniques, presented at VSTTE 2008 [12], provides an initial catalogue of bench-
mark challenges for the Verified Software Initiative. This paper presents solutions
to these eight benchmarks using the language and verifier Dafny. A Dafny pro-
gram includes specifications, code, inductive invariants, and termination metrics.
Each of the eight programs is fed to the Dafny verifier, which without further user
interaction automatically performs the verification in a few seconds.
1 The Challenge
The motivation from this work comes from the Verified Software Initiative [4] and the
suite of eight purposefully designed, incremental benchmarks for tools and techniques
to prove total correctness of sequential object-based and object-oriented software, as
presented by Weide et al. at VSTTE 2008 [12]. A solution to part of the first benchmark
is provided, while the main contribution of their paper is the provision of a benchmark
suite that aims to support the assessment of verification tools and the assessment of
techniques to prove total correctness of the functionality of software. The benchmark
suite also aims to provide for the evaluation of the state-of-the-art and to provide a
medium that allows researchers to illustrate and explain how proposed tools and tech-
niques deal with known pitfalls and well-understood issues, as well as how they can be
used to discover and attack new ones.
In this paper, we contribute to this assessment and evaluation by presenting our so-
lutions to the benchmark problems using the language and verifier Dafny [8,7]. The
full programs are available online at boogie.codeplex.com, located by browsing the
source code to access the folder Test/VSI-Benchmarks.
The benchmarks include several requirements of potential solutions, and we believe
we meet these:
– Our Dafny programs contain all formal specifications relevant to the benchmarks,
including user-defined mathematical functions where needed. Externally to the pro-
grams themselves, they rely only on constructs that are part of the Dafny language,
which include sets and sequences.
– The Dafny verifier produces verification conditions via the intermediate verification
language Boogie 2 [10,6]. The Boogie program and the resulting verification condi-
tions can be viewed by using, respectively, the /print and /proverLog switches of
G.T. Leavens, P. O’Hearn, and S.K. Rajamani (Eds.): VSTTE 2010, LNCS 6217, pp. 112–126, 2010.
c
© Springer-Verlag Berlin Heidelberg 2010

Dafny Meets the Verification Benchmarks Challenge 113
the Dafny verifier. For example, for the benchmark in the file b3.dfy, the command
dafny b3.dfy /print:b3.bpl /proverLog:b3.sx
writes out the intermediate Boogie program as b3.bpl and the theorem-prover in-
put, in S-expression form, as b3.sx.
– The Dafny verification system is described in a conference paper [8] and some
lecture notes [7].
– The Dafny verifier checks for total correctness (that is, including termination). It is
(designed to be) sound, which means it only proves correct programs to be correct.
The Dafny regression test suite (at boogie.codeplex.com) includes many exam-
ples of erroneous programs that, as expected, do not verify. Similarly, any change
to any part of our Dafny solution programs that renders them incorrect will cause
the verifier to no longer verify the programs.
– Dafny uses modular specifications and modular verification. That is, our solu-
tions need not be re-verified when they are incorporated as components in larger
programs.
– Finally, we have alerted the VSI repository of our solution programs (although we
have not seen them formally enter the repository yet).
2 Dafny
Dafny is an imperative, sequential language that supports user-defined generic classes
and algebraic datatypes [8,7]. The language includes specification constructs, like pre-
and postconditions à la Eiffel [11], JML [5], and Spec#[2,9]. In addition to instance
variables and methods, a class can define mathematical functions, which can be used
in specifications. Also, the language allows variables to be defined as ghost, meaning
they are used by the verifier but need not be present at run time.
The types supported by Dafny are booleans, mathematical integers, sets, sequences,
as well as user-defined classes and algebraic datatypes. Classes can be instantiated,
giving rise to object references (i.e., pointers), which makes the language useful for
many common applications. However, as an object-oriented language, Dafny does not
support subclasses and inheritance, except that the built-in type object is a supertype
of all class types. As such, the language Dafny could perhaps be construed as a more
modern version of Pascal or Euclid, or as a safe version of C.
The specification of a method consists of preconditions (introduced by the keyword
requires) and postconditions (keyword ensures), as well as a modification frame (key-
word modifies), which specifies which objects the method may modify, and a termi-
nation metric (keyword decreases), which gives a well-founded ranking function (also
known as a variant function) for proving termination. The specification of a function
consists of preconditions, which specify the domain of the function, a dependency frame
(keyword reads), which indicates on which objects the function’s value may depend,
and a termination metric.
The body of a method consists of an imperative statement, which includes standard
constructs like assignments, field updates, object allocation, conditional statements,
loops, and method calls. A loop can indicate an inductive loop invariant as well as a
termination metric. The body of a function is an expression that defines the value of the
function.