Most of this document describes the Dafny programming language.
This section describes the dafny tool, a combined verifier and compiler
that implements the Dafny language.
The development of the Dafny language and tool is a GitHub project at https://github.com/dafny-lang/dafny. The project is open source, with collaborators from various organizations; additional contributors are welcome. The software itself is licensed under the MIT license.
The dafny tool implements the following primary capabilities, implemented as various commands within the dafny tool:
- checking that the input files represent a valid Dafny program (i.e., syntax, grammar and name and type resolution);
- verifying that the program meets its specifications, by translating the program to verification conditions and checking those with Boogie and an SMT solver, typically Z3;
- compiling the program to a target language, such as C#, Java, Javascript, Go (and others in development);
- running the executable produced by the compiler.
In addition there are a variety of other capabilities, such as formatting files, also implemented as commands; more such commands are expected in the future.
The instructions for installing dafny and the required dependencies and environment
are described on the Dafny wiki:
https://github.com/dafny-lang/dafny/wiki/INSTALL.
They are not repeated here to avoid replicating information that
easily becomes inconsistent and out of date.
The dafny tool can also be installed using dotnet tool install --global dafny
(presuming that dotnet is already installed on your system).
Most users will find it most convenient to install the pre-built Dafny binaries available on the project release site or using the dotnet CLI.
As is typical for Open Source projects, dafny can also be built directly from the source files maintained in the github project.
Current and past Dafny binary releases can be found at https://github.com/dafny-lang/dafny/releases for each supported platform. Each release is a .zip file with a name combining the release name and the platform. Current platforms are Windows 11, Ubuntu 20 and later, and MacOS 10.14 and later.
The dafny tool is distributed as a standalone executable. A compatible version of the required Z3 solver is included in the release. There are additional dependencies that are needed to compile dafny to particular target languages, as described in the release instructions. A development environment to build dafny from source requires additional dependencies, described here.
Dafny source files are text files and can of course be edited with any text editor. However, some tools provide syntax-aware features:
- VSCode, a cross-platform editor for many programming languages has an extension for Dafny. VSCode is available here and the Dafny extension can be installed from within VSCode. The extension provides syntax highlighting, in-line parser, type and verification errors, code navigation, counter-example display and gutter highlights.
- There is a Dafny mode for Emacs.
- An old Visual Studio plugin is no longer supported
Information about installing IDE extensions for Dafny is found on the Dafny INSTALL page in the wiki.
More information about using VSCode IDE is here.
A Dafny program is a set of modules.
Modules can refer to other modules, such as through import declarations
or refines clauses.
A Dafny program consists of all the modules needed so that all module
references are resolved.
Dafny programs are contained in files that have a .dfy suffix.
Such files each hold
some number of top-level declarations. Thus a full program may be
distributed among multiple files.
To apply the dafny tool to a Dafny program, the dafny tool must be
given all the files making up a complete program (or, possibly, more than
one program at a time). This can be effected either by listing all of the files
by name on the command-line or by using include directives within a file
to stipulate what other files contain modules that the given files need.
Thus the complete set of modules are all the modules in all the files listed
on the command-line or referenced, recursively, by include directives
within those files. It does not matter if files are repeated either as
includes or on the command-line.1
All files recursively included are always parsed and type-checked. However, which files are verified, built, run, or processed by other dafny commands depends on the individual command. These commands are described in Section 13.6.1.
As of Dafny 4.1, dafny now supports outputting a single file containing
a fully-verified program along with metadata about how it was verified.
Such files use the extension .doo, for Dafny Output Object,
and can be used as input anywhere a .dfy file can be.
.doo files are produced by an additional backend called the "Dafny Library" backend,
identified with the name lib on the command line. For example, to build multiple
Dafny files into a single build artifact for shared reuse, the command would look something like:
dafny build -t:lib A.dfy B.dfy C.dfy --output:MyLib.dooThe Dafny code contained in a .doo file is not re-verified when passed back to the dafny tool,
just as included files and those passed with the --library option are not.
Using .doo files provides a guarantee that the Dafny code was in fact verified,
however, and therefore offers protection against build system mistakes.
.doo files are therefore ideal for sharing Dafny libraries between projects.
.doo files also contain metadata about the version of Dafny used to verify them
and the values of relevant options that affect the sound separate verification and
compilation of Dafny code, such as --unicode-char.
This means attempting to use a library that was built with options
that are not compatible with the currently executing command options
will lead to errors.
This also includes attempting to use a .doo file built with a different version of Dafny,
although this restriction may be lifted in the future.
A .doo file is a compressed archive of multiple files, similar to the .jar file format for Java packages.
The exact file format is internal and may evolve over time to support additional features.
Note that the library backend only supports the newer command-style CLI interface.
Some options, such as --outer-module or --optimize-erasable-datatype-wrapper,
affect what target language code the same Dafny code is translated to.
In order to translate Dafny libraries separately from their consuming codebases,
the translation process for consuming code needs to be aware
of what options were used when translating the library.
For example, if a library defines a Foo() function in an A module,
but --outer-module org.coolstuff.foolibrary.dafnyinternal is specified when translating the library to Java,
then a reference to A.Foo() in a consuming Dafny project
needs to be translated to org.coolstuff.foolibrary.dafnyinternal.A.Foo(),
independently of what value of --outer-module is used for the consuming project.
To meet this need,
dafny translate also outputs a <program-name>-<target id>.dtr Dafny Translation Record file.
Like .doo files, .dtr files record all the relevant options that were used,
in this case relevant to translation rather than verification.
These files can be provided to future calls to dafny translate using the --translation-record option,
in order to provide the details of how various libraries provided with the --library flag were translated.
Currently --outer-module is the only option recorded in .dtr files,
but more relevant options will be added in the future.
A later version of Dafny will also require .dtr files that cover all modules
that are defined in --library options,
to support checking that all relevant options are compatible.
As of Dafny 4.4, the dafny tool includes standard libraries that any Dafny code base can depend on.
For now they are only available when the --standard-libraries option is provided,
but they will likely be available by default in the next major version of Dafny.
See https://github.com/dafny-lang/dafny/blob/master/Source/DafnyStandardLibraries/README.md for details.
There are coding style conventions for Dafny code, recorded here. Most significantly, code is written without tabs and with a 2 space indentation. Following code style conventions improves readability but does not alter program semantics.
dafny is a conventional command-line tool, operating just like other
command-line tools in Windows and Unix-like systems.
In general, the format of a command-line is determined by the shell program that is executing the command-line
(.e.g., bash, the windows shell, COMMAND, etc.),
but is expected to be a series of space-separated "words", each representing a command, option, option argument, file, or folder.
As of v3.9.0, dafny uses a command-style command-line (like git for example); prior to v3.9.0, the
command line consisted only of options and files.
It is expected that additional commands will be added in the future.
Each command may have its own subcommands and its own options, in addition to generally applicable options.
Thus the format of the command-line is
a command name, followed by options and files:
dafny <command> <options> <files>;
the command-name must be the first command-line argument.
The command-line dafny --help or dafny -h lists all the available commands.
The command-line dafny <command> --help (or -h or -?) gives help information for that particular <command>, including the list of options.
Some options for a particular command are intended only for internal tool development; those are shown using the --help-internal option instead of --help.
Also, the command-style command-line has modernized the syntax of options; they are now POSIX-compliant.
Like many other tools, options now typically begin with a double hyphen,
with some options having a single-hyphen short form, such as --help and -h.
If no <command> is given, then the command-line is presumed to use old-style syntax, so any previously written command-line will still be valid.
dafny recognizes the commands described in the following subsections. The most commonly used
are dafny verify, dafny build, and dafny run.
The command-line also expects the following:
- Files are designated by absolute paths or paths relative to the current working directory. A command-line argument not matching a known option is considered a filepath, and likely one with an unsupported suffix, provoking an error message.
- Files containing dafny code must have a
.dfysuffix. - There must be at least one
.dfyfile (except when using--stdinor in the case ofdafny format, see the Dafny format section) - The command-line may contain other kinds of files appropriate to the language that the Dafny files are being compiled to. The kind of file is determined by its suffix.
- Escape characters are determined by the shell executing the command-line.
- Per POSIX convention, the option
--means that all subsequent command-line arguments are not options to the dafny tool; they are either files or arguments to thedafny runcommand. - If an option is repeated (e.g., with a different argument), then the later instance on the command-line supersedes the earlier instance, with just a few options accumulating arguments.
- If an option takes an argument, the option name is followed by a
:or=or whitespace and then by the argument value; if the argument itself contains white space, the argument must be enclosed in quotes. It is recommended to use the:or=style to avoid misinterpretation or separation of a value from its option. - Boolean options can take the values
trueandfalse(or any case-insensitive version of those words). For example, the value of--no-verifyis by defaultfalse(that is, do verification). It can be explicitly set to true (no verification) using--no-verify,--no-verify:true,--no-verify=true,--noverify true; it can be explicitly set false (do verification) using--no-verify:falseor--no-verify=falseor--no-verify false. - There is a potential ambiguity when the form
--option valueis used if the value is optional (such as for boolean values). In such a case an argument after an option (that does not have an argument given with:or=) is interpreted as the value if it is indeed a valid value for that option. However, better style advises always using a ':' or '=' to set option values. No valid option values in dafny look like filenames or begin with--.
A few options are not part of a command. In these cases any single-hyphen spelling also permits a spelling beginning with '/'.
dafny --helpordafny -hlists all the available commandsdafny -?ordafny -helplist all legacy optionsdafny --version(or-version) prints out the number of the version this build of dafny implements
The dafny resolve command checks the command-line and then parses and typechecks the given files and any included files.
The set of files considered by dafny are those listed on the command-line,
including those named in a --library option, and all files that are
named, recursively, in include directives in files in the set being considered by the tool.
The set of files presented to an invocation of the dafny tool must
contain all the declarations needed to resolve all names and types,
else name or type resolution errors will be emitted.
dafny can parse and verify sets of files that do not form a
complete program because they are missing the implementations of
some constructs such as functions, lemmas, and loop bodies.2
However, dafny will need all implementations in order to compile a working executable.
The options relevant to this command are
-
those relevant to the command-line itself
--allow-warnings--- return a success exit code, even when there are warnings
-
those that affect dafny` as a whole, such as
--cores--- set the number of cores dafny should use--show-snippets--- emit a line or so of source code along with an error message--library--- include this file in the program, but do not verify or compile it (multiple such library files can be listed using multiple instances of the--libraryoption)--stdin-- read from standard input
-
those that affect the syntax of Dafny, such as
--prelude--unicode-char--function-syntax--quantifier-syntax--track-print-effects--warn-shadowing--warn-missing-constructor-parentheses
The dafny verify command performs the dafny resolve checks and then attempts to verify each declaration in the program.
A guide to controlling and aiding the verification process is given in a later section.
To be considered verified all the methods in all the files in a program must be verified, with consistent sets of options,
and with no unproven assumptions (see dafny audit for a tool to help identify such assumptions).
Dafny works modularly, meaning that each method is considered by itself, using only the specifications of other methods. So, when using the dafny tool, you can verify the program all at once or one file at a time or groups of files at a time. On a large program, verifying all files at once can take quite a while, with little feedback as to progress, though it does save a small amount of work by parsing all files just once. But, one way or another, to have a complete verification, all implementations of all methods and functions must eventually be verified.
- By default, only those files listed on the command-line are verified in a given invocation of the
dafnytool. - The option
--verify-included-files(-verifyAllModulesin legacy mode) forces the contents of all non-library files to be verified, whether they are listed on the command-line or recursively included by files on the command-line. - The
--libraryoption marks files that are excluded from--verify-included-files. Such a file may also, but need not, be the target of anincludedirective in some file of the program; in any case, such files are included in the program but not in the set of files verified (or compiled). The intent of this option is to mark files that should be considered as libraries that are independently verified prior to being released for shared use. - Verifying files individually is equivalent to verifying them in groups, presuming no other changes.
It is also permitted to verify completely disjoint files or
programs together in a single run of
dafny.
Various options control the verification process, in addition to all those described for dafny resolve.
-
What is verified
--verify-included-files(when enabled, all included files are verified, except library files, otherwise just those files on the command-line)--relax-definite-assignment--track-print-effects--disable-nonlinear-arithmetic--filter-symbol
-
Control of the proof engine
--manual-lemma-induction--verification-time-limit--boogie--solver-path
The dafny translate command translates Dafny source code to source code for another target programming language.
The command always performs the actions of dafny resolve and, unless the --no-verify option is specified, does the actions of dafny verify.
The language is designated by a subcommand argument, rather than an option, and is required.
The current set of supported target languages is
- cs (C#)
- java (Java)
- js (JavaScript)
- py (Python)
- go (Go)
- cpp (C++ -- but only limited support)
In addition to generating the target source code, dafny may generate build artifacts to assist in compiling the generated code.
The specific files generated depend on the target programming language.
More detail is given in the section on compilation.
The dafny tool intends that the compiled program in the target language be a semantically faithful rendering of the
(verified) Dafny program. However, resource and language limitations make this not always possible.
For example, though Dafny can express and reason about arrays of unbounded size,
not all target programming languages can represent arrays larger than the maximum signed 32-bit integer.
Various options control the translation process, in addition to all those described for dafny resolve and dafny verify.
-
General options:
--no-verify--- turns off all attempts to verify the program--verbose--- print information about generated files
-
The translation results
--output(or-o) --- location of the generated file(s) (this specifies a file path and name; a folder location for artifacts is derived from this name)--include-runtime--- include the Dafny runtime for the target language in the generated artifacts--optimize-erasable-datatype-wrapper--enforce-determinism--test-assumptions--- (experimental) inserts runtime checks for unverified assumptions when they are compilable
The dafny build command runs dafny translate and then compiles the result into an executable artifact for the target platform,
such as a .exe or .dll or executable .jar, or just the source code for an interpreted language.
If the Dafny program does not have a Main entry point, then the build command creates a library, such as a .dll or .jar.
As with dafny translate, all the previous phases are also executed, including verification (unless --no-verify is a command-line option).
By default, the generated file is in the same directory and has the same name with a different extension as the first
.dfy file on the command line. This location and name can be set by the --output option.
The location of the Main entry point is described [here](#sec-user-guide-main}.
There are no additional options for dafny build beyond those for dafny translate and the previous compiler phases.
Note that dafny build may do optimizations that dafny run does not.
Details for specific target platforms are described in Section 25.7.
The dafny run command compiles the Dafny program and then runs the resulting executable.
Note that dafny run is engineered to quickly compile and launch the program;
dafny build may take more time to do optimizations of the build artifacts.
The form of the dafny run command-line is slightly different than for other commands.
- It permits just one
.dfyfile, which must be the file containing theMainentry point; the location of theMainentry point is described [here](#sec-user-guide-main}. - Other files are included in the program either by
includedirectives within that one file or by the--inputoption on the command-line. - Anything that is not an option and is not that one dfy file is an argument to the program being run (and not to dafny itself).
- If the
--option is used, then anything after that option is a command-line argument to the program being run.
During development, users must use dafny run --allow-warnings if they want to run their Dafny code when it contains warnings.
Here are some examples:
dafny run A.dfy-- builds and runs the Main program inA.dfywith no command-line argumentsdafny run A.dfy --no-verify-- builds the Main program inA.dfyusing the--no-verifyoption, and then runs the program with no command-line argumentsdafny run A.dfy -- --no-verify-- builds the Main program inA.dfy(not using the--no-verifyoption), and then runs the program with one command-line argument, namely--no-verifydafny run A.dfy 1 2 3 B.dfy-- builds the Main program inA.dfyand then runs it with the four command-line arguments1 2 3 B.dfydafny run A.dfy 1 2 3 --input B.dfy-- builds the Main program inA.dfyandB.dfy, and then runs it with the three command-line arguments1 2 3dafny run A.dfy 1 2 -- 3 -quiet-- builds the Main program inA.dfyand then runs it with the four command-line arguments1 2 3 -quiet
Each time dafny run is invoked, the input Dafny program is compiled before it is executed.
If a Dafny program should be run more than once, it can be faster to use dafny build,
which enables compiling a Dafny program once and then running it multiple times.
Note: dafny run will typically produce the same results as the executables produced by dafny build. The only expected differences are these:
- performance ---
dafny runmay not optimize as much asdafny build - target-language-specific configuration issues --- e.g. encoding issues:
dafny runsets language-specific flags to request UTF-8 output for theprintstatement in all languages, whereasdafny buildleaves language-specific runtime configuration to the user.
The dafny server command starts the Dafny Language Server, which is an LSP-compliant implementation of Dafny.
The Dafny VSCode extension uses this LSP implementation, which in turn uses the same core Dafny implementation as the command-line tool.
The Dafny Language Server is described in more detail here.
The dafny audit command reports issues in the Dafny code that might limit the soundness claims of verification.
This command is under development.
The command executes the dafny resolve phase (accepting its options) and has the following additional options:
--report-file:<report-file>--- specifies the path where the audit report file will be stored. Without this option, the report will be issued as standard warnings, written to standard-out.--report-format:<format>--- specifies the file format to use for the audit report. Supported options include:- 'txt, 'text': plain text in the format of warnings
- 'html': standalone HTML ('html')
- 'md', 'markdown', 'md-table', 'markdown-table': a Markdown table
- 'md-ietf', 'markdown-ietf': an IETF-language document in Markdown format
- The default is to infer the format from the filename extension
--compare-report--- compare the report that would have been generated with the existing file given by --report-file, and fail if they differ.
The command emits exit codes of
- 1 for command-line errors
- 2 for parsing, type-checking or serious errors in running the auditor (e.g. failure to write a report or when report comparison fails)
- 0 for normal operation, including operation that identifies audit findings
It also takes the --verbose option, which then gives information about the files being formatted.
The dafny audit command currently reports the following:
-
Any declaration marked with the
{:axiom}attribute. This is typically used to mark that a lemma with no body (and is therefore assumed to always be true) is intended as an axiom. The key purpose of theauditcommand is to ensure that all assumptions are intentional and acknowledged. To improve assurance, however, try to provide a proof. -
Any declaration marked with the
{:verify false}attribute, which tells the verifier to skip verifying this declaration. Removing the attribute and providing a proof will improve assurance. -
Any declaration marked with the
{:extern}attribute that has at least onerequiresorensuresclause. If code implemented externally, and called from Dafny, has anensuresclause, Dafny assumes that it satisfies that clause. Since Dafny cannot prove properties about code written in other languages, adding tests to provide evidence that anyensuresclauses do hold can improve assurance. The same considerations apply torequiresclauses on Dafny code intended to be called from external code. -
Any definition with an
assumestatement in its body. To improve assurance, attempt to convert it to anassertstatement and prove that it holds. Such a definition will not be compilable unless the statement is also marked with{:axiom}. Alternatively, converting it to anexpectstatement will cause it to be checked at runtime. -
Any method marked with
decreases *. Such a method may not terminate. Although this cannot cause an unsound proof, in the logic of Dafny, it's generally important that any non-termination be intentional. -
Any
forallstatement without a body. This is equivalent to an assumption of its conclusion. To improve assurance, provide a body that proves the conclusion. -
Any loop without a body. This is equivalent to an assumption of any loop invariants in the code after the loop. To improve assurance, provide a body that establishes any stated invariants.
-
Any declaration with no body and at least one
ensuresclause. Any code that calls this declaration will assume that allensuresclauses are true after it returns. To improve assurance, provide a body that proves that anyensuresclauses hold.
Dafny supports a formatter, which for now only changes the indentation of lines in a Dafny file, so that it conforms to the idiomatic Dafny code formatting style. For the formatter to work, the file should be parsed correctly by Dafny.
There are four ways to use the formatter:
dafny format <one or more .dfy files or folders>formats the given Dafny files and the Dafny files in the folders, recursively, altering the files in place. For example,dafny format .formats all the Dafny files recursively in the current folder.dafny format --print <files and/or folders>formats each file but instead of altering the files, output the formatted content to stdoutdafny format --check <files and/or folders>does not alter files. It will print a message concerning which files need formatting and return a non-zero exit code if any files would be changed by formatting.
You can also use --stdin instead of providing a file, to format a full Dafny file from the standard input.
Input files can be named along with --stdin, in which case both the files and the content of the stdin are formatted.
Each version of dafny format returns a non-zero return code if there are any command-line or parsing
errors or if --check is stipulated and at least one file is not the same as its formatted version.
dafny format does not necessarily report name or type resolution errors and does not attempt verification.
This command (verifies and compiles the program and) runs every method in the program that is annotated with the {:test} attribute.
Verification can be disabled using the --no-verify option. dafny test also accepts all other options of the dafny build command.
In particular, it accepts the --target option that specifies the programming language used in the build and execution phases.
dafny test also accepts these options:
-spill-translation- (default disabled) when enabled the compilation artifacts are retained--output- gives the folder and filename root for compilation artifacts--methods-to-test- the value is a (.NET) regular expression that is matched against the fully qualified name of the method; only those methods that match are tested--coverage-report- the value is a directory in which Dafny will save an html coverage report highlighting parts of the program that execution of the tests covered.
The order in which the tests are run is not specified.
For example, this code (as the file t.dfy)
method {:test} m() {
mm();
print "Hi!\n";
}
method mm() {
print "mm\n";
}
module M {
method {:test} q() {
print 42, "\n";
}
}
class A {
static method {:test} t() { print "T\n"; }
}and this command-line
dafny test --no-verify t.dfyproduce this output text:
M.q: 42
PASSED
A.t: T
PASSED
m: mm
Hi!
PASSED
and this command-line
dafny test --no-verify --methods-to-test='m' t.dfyproduces this output text:
m: mm
Hi!
PASSED
The dafny doc command generates HTML documentation pages describing the contents of each
module in a set of files, using the documentation comments in the source files.
This command is experimental; user feedback and contributor PRs on the layout of information and the navigation are welcome.
- The format of the documentation comments is described here.
- The
dafny doccommand accepts either files or folders as command-line arguments. A folder represents all the.dfyfiles contained recursively in that folder. A file that is a.tomlproject file represents all the files and options listed in the project file. - The command first parses and resolves the given files; it only proceeds to produce documentation
if type resolution is successful (on all files). All the command-line options relevant to
dafny resolveare available fordafny doc. - The value of the
--outputoption is a folder in which all the generated files will be placed. The default location is./docs. The folder is created if it does not already exist. Any existing content of the folder is overwritten. - If
--verboseis enabled, a list of the generated files is emitted to stdout. - The output files contain information stating the source .dfy file in which the module is
declared. The
--file-nameoption controls the form of the filename in that information:- --file-name:none -- no source file information is emitted
- --file-name:name -- (default) just the file name is emitted (e.g.,
Test.dfy) - --file-name:absolute -- an absolute full path is emitted
- --file-name:relative= -- a file name relative to the given prefix is emitted
- If
--modify-timeis enabled, then the generated files contain information stating the last modified time of the source of the module being documented. - The
--program-nameoption states text that will be included in the heading of the TOC and index pages
The output files are HTML files, all contained in the given folder, one per module plus an
index.html file giving an overall table of contents and a nameindex.html file containing
an alphabetical by name list of all the declarations in all the modules.
The documentation for the root module is in _.html.
This experimental command allows generating tests from Dafny programs.
The tests provide complete coverage of the implementation and one can execute them using the dafny test command.
Dafny can target different notions of coverage while generating tests, with basic-block coverage being the recommended setting.
Basic blocks are extracted from the Boogie representation of the Dafny program, with one basic block corresponding
to a statement or a non-short-circuiting subexpression in the Dafny code. The underlying implementation uses the
verifier to reason about the reachability of different basic blocks in the program and infers necessary test inputs
from counterexamples.
For example, this code (as the file program.dfy)
module M {
function {:testEntry} Min(a: int, b: int): int {
if a < b then a else b
}
}and this command-line
dafny generate-tests Block program.dfyproduce two tests:
include "program.dfy"
module UnitTests {
import M
method {:test} Test0() {
var r0 := M.Min(0, 0);
}
method {:test} Test1() {
var r0 := M.Min(0, 1);
}
}The two tests together cover every basic block within the Min function in the input program.
Note that the Min function is annotated with the {:testEntry} attribute. This attribute marks Min as
the entry point for all generated tests, and there must always be at least one method or function so annotated.
Another requirement is that any top-level declaration that is not itself a module (such as class, method, function,
etc.) must be a member of an explicitly named module, which is called M in the example above.
This command is under development and not yet fully functional.
By default, when asked to generate tests, Dafny will produce unit tests, which guarantee coverage of basic blocks
within the method they call but not within any of its callees. By contrast, system-level tests can
guarantee coverage of a large part of the program while at the same time using a single method as an entry point.
In order to prompt Dafny to generate system-level tests, one must use the {:testInline} attribute.
For example, this code (as the file program.dfy)
module M {
function {:testInline} Min(a: int, b: int): int {
if a < b then a else b
}
method {:testEntry} Max(a: int, b: int) returns (c: int)
// the tests convert the postcondition below into runtime check:
ensures c == if a > b then a else b
{
return -Min(-a, -b);
}
}and this command-line
dafny generate-tests Block program.dfyproduce two tests:
include "program.dfy"
module UnitTests {
import M
method {:test} Test0() {
var r0 := M.Max(7719, 7720);
expect r0 == if 7719 > 7720 then 7719 else 7720;
}
method {:test} Test1() {
var r0 := M.Max(1, 0);
expect r0 == if 1 > 0 then 1 else 0;
}
}Without the use of the {:testInline} attribute in the example above, Dafny will only generate a single test
because there is only one basic-block within the Max method itself -- all the branching occurs within the Min function.
Note also that Dafny automatically converts all non-ghost postconditions on the method under tests into expect statements,
which the compiler translates to runtime checks in the target language of choice.
When the inlined method or function is recursive, it might be necessary to unroll the recursion several times to
get adequate code coverage. The depth of recursion unrolling should be provided as an integer argument to the {:testInline}
attribute. For example, in the program below, the function Mod3 is annotated with {:testInline 2} and
will, therefore, be unrolled twice during test generation. The function naively implements division by repeatedly and
recursively subtracting 3 from its argument, and it returns the remainder of the division, which is one of
the three base cases. Because the TestEntry method calls Mod3 with an argument that is guaranteed to be at least 3,
the base case will never occur on first iteration, and the function must be unrolled at least twice for Dafny to generate
tests covering any of the base cases:
module M {
function {:testInline 2} Mod3 (n: nat): nat
decreases n
{
if n == 0 then 0 else
if n == 1 then 1 else
if n == 2 then 2 else
Mod3(n-3)
}
method {:testEntry} TestEntry(n: nat) returns (r: nat)
requires n >= 3
{
r := Mod3(n);
}
}Test generation supports a number of command-line options that control its behavior.
The first argument to appear after the generate-test command specifies the coverage criteria Dafny will attempt to satisfy.
Of these, we recommend basic-block coverage (specified with keyword Block), which is also the coverage criteria used
throughout the relevant parts of this reference manual. The alternatives are path coverage (Path) and block coverage
after inlining (InlinedBlock). Path coverage provides the most diverse set of tests but it is also the most expensive
in terms of time it takes to produce these tests. Block coverage after inlining is a call-graph sensitive version of
block coverage - it takes into account every block in a given method for every path through the call-graph to that method.
The following is a list of command-line-options supported by Dafny during test generation:
--verification-time-limit- the value is an integer that sets a timeout for generating a single test. The default is 20 seconds.--length-limit- the value is an integer that is used to limit the lengths or all sequences and sizes of all maps and sets that test generation will consider as valid test inputs. This can sometimes be necessary to prevent test generation from creating unwieldy tests with excessively long strings or large maps. This option is disabled by default--coverage-report- the value is a directory in which Dafny will save an html coverage report highlighting parts of the program that the generated tests are expected to cover.--print-bpl- the value is the name of the file to which Dafny will save the Boogie code used for generating tests. This options is mostly useful for debugging test generation functionality itself.--force-prune- this flag enables axiom pruning, a feature which might significantly speed up test generation but can also reduce coverage or cause Dafny to produce tests that do not satisfy the preconditions.
Dafny will also automatically enforce the following options during test generation: --enforce-determinism,
/typeEncoding:p (an option passed on to Boogie).
This experimental command finds dead code in a program, that is, basic-blocks within a method that are not reachable
by any inputs that satisfy the method's preconditions. The underlying implementation is identical to that of
dafny generate-tests command and can be controlled by the same command line options and method
attributes.
For example, this code (as the file program.dfy)
module M {
function {:testEntry} DescribeProduct(a: int): string {
if a * a < 0
then "Product is negative"
else "Product is nonnegative"
}
}and this command-line
dafny find-dead-code program.dfyproduce this output:
program.dfy(5,9) is reachable.
program.dfy(3,4):initialstate is reachable.
program.dfy.dfy(5,9)#elseBranch is reachable.
program.dfy.dfy(4,9)#thenBranch is potentially unreachable.
Out of 4 basic blocks, 3 are reachable.
Dafny reports that the then branch of the condition is potentially unreachable because the verifier proves that no
input can reach it. In this case, this is to be expected, since the product of two numbers can never be negative. In
practice, find-dead-code command can produce both false positives (if the reachability query times out) and false
negatives (if the verifier cannot prove true unreachability), so the results of such a report should always be
reviewed.
This command is under development and not yet fully functional.
This experimental command reports complexity metrics of a program.
This command is under development and not yet functional.
This execution mode is not a command, per se, but rather a command-line option that enables executing plugins to the dafny tool. Plugins may be either standalone tools or be additions to existing commands.
The form of the command-line is dafny --plugin:<path-to-one-assembly[,argument]*> or dafny <command> --plugin:<path-to-one-assembly[,argument]*>
where the argument to --plugin gives the path to the compiled assembly of the plugin and the arguments to be provided to the plugin.
More on writing and building plugins can be found in this section.
Prior to implementing the command-based CLI, the dafny command-line simply took files and options and the arguments to options.
That legacy mode of operation is still supported, though discouraged. The command dafny -? produces the list of legacy options.
In particular, the common commands like dafny verify and dafny build are accomplished with combinations of
options like -compile, -compileTarget and -spillTargetCode.
Users are encouraged to migrate to the command-based style of command-lines and the double-hyphen options.
As is typical for command-line tools, dafny provides in-tool help through the -h and --help options:
dafny -h,dafny --helplist the commands available in thedafnytooldafny -?lists all the (legacy) options implemented indafnydafny <command> -h,dafny <command> --help,dafny <command> -?list the options available for that command
The basic resolve, verify, translate, build, run and commands of dafny terminate with these exit codes.
- 0 -- success
- 1 -- invalid command-line arguments
- 2 -- syntax, parse, or name or type resolution errors
- 3 -- compilation errors
- 4 -- verification errors
Errors in earlier phases of processing typically hide later errors. For example, if a program has parsing errors, verification or compilation will not be attempted.
Other dafny commands may have their own conventions for exit codes. However in all cases, an exit code of 0 indicates successful completion of the command's task and small positive integer values indicate errors of some sort.
Most output from dafny is directed to the standard output of the shell invoking the tool, though some goes to standard error.
- Command-line errors: these are produced by the dotnet CommandLineOptions package are directed to standard-error
- Other errors: parsing, typechecking, verification and compilation errors are directed to standard-out
- Non-error progress information also is output to standard-out
- Dafny
printstatements, when executed, send output to standard-out - Dafny
expectstatements (when they fail) send a message to standard-out. - Dafny I/O libraries send output explicitly to either standard-out or standard-error
Commands on the Dafny CLI that can be passed a Dafny file can also be passed a Dafny project file. Such a project file may define which Dafny files the project contains and which Dafny options it uses. The project file must be a TOML file named dfyconfig.toml for it to work on both the CLI and in the Dafny IDE, although the CLI will accept any .toml file.
Here's an example of a Dafny project file:
includes = ["src/**/*.dfy"]
excludes = ["**/ignore.dfy"]
base = ["../commonOptions.dfyconfig.toml"]
[options]
enforce-determinism = true
warn-shadowing = true-
At most one
.tomlfile may be named on the command-line; when using the command-line no.tomlfile is used by default. -
In the
includesandexcludeslists, the file paths may have wildcards, including**to mean any number of directory levels; filepaths are relative to the location of the.tomlfile in which they are named. -
Dafny will process the union of (a) the files on the command-line and (b) the files designated in the
.tomlfile, which are those specified by theincludes, omitting those specified by theexcludes. Theexcludesdoes not remove any files that are listed explicitly on the command-line. -
Under the section
[options], any options from the Dafny CLI can be specified using the option's name without the--prefix. -
When executing a
dafnycommand using a project file, any options specified in the file that can be applied to the command, will be. Options that can't be applied are ignored; options that are invalid for any dafny command trigger warnings. -
Options specified on the command-line take precedence over any specified in the project file, no matter the order of items on the command-line.
-
When using a Dafny IDE based on the
dafny servercommand, the IDE will search for project files by traversing up the file tree looking for the closestdfyconfig.tomlfile to the dfy being parsed that it can find. Options from the project file will override options passed todafny server. -
The field 'base' can be used to let one project file inherit options from another. If an option is specified in both, then the value specified in the inheriting project is used. Includes from the inheritor override excludes from the base.
It's not possible to use Dafny project files in combination with the legacy CLI UI.
In this section, we suggest a methodology to figure out why a single assertion might not hold, we propose techniques to deal with assertions that slow a proof down, we explain how to verify assertions in parallel or in a focused way, and we also give some more examples of useful options and attributes to control verification.
Let's assume one assertion is failing ("assertion might not hold" or "postcondition might not hold"). What should you do next?
The following section is textual description of the animation below, which illustrates the principle of debugging an assertion by computing the weakest precondition:
Let's look at an example of a failing postcondition.
method FailingPostcondition(b: bool) returns (i: int)
ensures 2 <= i
{
var j := if !b then 3 else 1;
if b {
return j;
}//^^^^^^^ a postcondition might not hold on this return path.
i := 2;
}One first thing you can do is replace the statement return j; by two statements i := j; return; to better understand what is wrong:
method FailingPostcondition(b: bool) returns (i: int)
ensures 2 <= i
{
var j := if !b then 3 else 1;
if b {
i := j;
return;
}//^^^^^^^ a postcondition might not hold on this return path.
i := 2;
}Now, you can assert the postcondition just before the return:
method FailingPostcondition(b: bool) returns (i: int)
ensures 2 <= i
{
var j := if !b then 3 else 1;
if b {
i := j;
assert 2 <= i; // This assertion might not hold
return;
}
i := 2;
}That's it! Now the postcondition is not failing anymore, but the assert contains the error!
you can now move to the next section to find out how to debug this assert.
In the previous section, we arrived at the point where we have a failing assertion:
method FailingPostcondition(b: bool) returns (i: int)
ensures 2 <= i
{
var j := if !b then 3 else 1;
if b {
i := j;
assert 2 <= i; // This assertion might not hold
return;
}
i := 2;
}To debug why this assert might not hold, we need to move this assert up, which is similar to computing the weakest precondition.
For example, if we have x := Y; assert F; and the assert F; might not hold, the weakest precondition for it to hold before x := Y; can be written as the assertion assert F[x:= Y];, where we replace every occurrence of x in F into Y.
Let's do it in our example:
method FailingPostcondition(b: bool) returns (i: int)
ensures 2 <= i
{
var j := if !b then 3 else 1;
if b {
assert 2 <= j; // This assertion might not hold
i := j;
assert 2 <= i;
return;
}
i := 2;
}Yay! The assertion assert 2 <= i; is not proven wrong, which means that if we manage to prove assert 2 <= j;, it will work.
Now, this assert should hold only if we are in this branch, so to move the assert up, we need to guard it.
Just before the if, we can add the weakest precondition assert b ==> (2 <= j):
method FailingPostcondition(b: bool) returns (i: int)
ensures 2 <= i
{
var j := if !b then 3 else 1;
assert b ==> 2 <= j; // This assertion might not hold
if b {
assert 2 <= j;
i := j;
assert 2 <= i;
return;
}
i := 2;
}Again, now the error is only on the topmost assert, which means that we are making progress.
Now, either the error is obvious, or we can one more time replace j by its value and create the assert assert b ==> ((if !b then 3 else 1) >= 2);
method FailingPostcondition(b: bool) returns (i: int)
ensures 2 <= i
{
assert b ==> 2 <= (if !b then 3 else 1); // This assertion might not hold
var j := if !b then 3 else 1;
assert b ==> 2 <= j;
if b {
assert 2 <= j;
i := j;
assert 2 <= i;
return;
}
i := 2;
}At this point, this is pure logic. We can simplify the assumption:
b ==> 2 <= (if !b then 3 else 1)
!b || (if !b then 2 <= 3 else 2 <= 1)
!b || (if !b then true else false)
!b || !b;
!b;Now we can understand what went wrong: When b is true, all of these formulas above are false, this is why the dafny verifier was not able to prove them.
In the next section, we will explain how to "move asserts up" in certain useful patterns.
This list is not exhaustive but can definitely be useful to provide the next step to figure out why Dafny could not prove an assertion.
| Failing assert | Suggested rewriting |
|---|---|
x := Y;assert P; |
assert P[x := Y];x := Y;assert P; |
if B { assert P; ...} |
assert B ==> P;if B { assert P; ...} |
if B { ...} else { assert P; ...} |
assert !B ==> P;if B { ...} else { assert P; ...} |
if X { ...} else { ...}assert A; |
if X { ... assert A;} else { ... assert A;}assert A; |
assert forall x :: Q(x); |
forall x ensures Q(x){ assert Q(x);}; assert forall x :: Q(x); |
assert forall x :: P(x) ==> Q(x); |
[`forall x |
`assert exists x |
P(x) :: Q(x);<br>assert exists x |
assert exists x :: P(x); |
assert P(x0);assert exists x :: P(x);for a given expression x0. |
ensures exists i :: P(i); |
returns (j: int)ensures P(j) ensures exists i :: P(i)in a lemma, so that the j can be computed explicitly. |
assert A == B;callLemma(x);assert B == C; |
calc == { A; B; { callLemma(x); } C;};assert A == B;where the calc statement can be used to make intermediate computation steps explicit. Works with <, >, <=, >=, ==>, <== and <==> for example. |
assert A ==> B; |
if A { assert B;};assert A ==> B; |
assert A && B; |
assert A;assert B;assert A && B; |
ensures P ==> Q on a lemma |
requires P ensures Q to avoid accidentally calling the lemma on inputs that do not satisfy P |
seq(size, i => P) |
seq(size, i requires 0 <= i < size => P); |
assert forall x :: G(i) ==> R(i); |
assert G(i0);assert R(i0);assert forall i :: G(i) ==> R(i); with a guess of the i0 that makes the second assert to fail. |
`assert forall i |
0 < i <= m :: P(i);` |
`assert forall i |
i == m :: P(m);` |
method m(i) returns (j: T) requires A(i) ensures B(i, j){ ...}method n() { ... var x := m(a); assert P(x); |
method m(i) returns (j: T) requires A(i) ensures B(i, j){ ...}method n() { ... assert A(k); assert forall x :: B(k, x) ==> P(x); var x := m(k); assert P(x); |
method m_mod(i) returns (j: T) requires A(i) modifies this, i ensures B(i, j){ ...}method n_mod() { ... var x := m_mod(a); assert P(x); |
method m_mod(i) returns (j: T) requires A(i) modifies this, i ensures B(i, j){ ...}method n_mod() { ... assert A(k); modify this, i; // Temporarily var x: T; // Temporarily assume B(k, x);// var x := m_mod(k); assert P(x); |
modify x, y;assert P(x, y, z); |
assert x != z && y != z;modify x, y;assert P(x, y, z); |
When verification fails, we can rerun Dafny with --extract-counterexample flag to get a counterexample that can potentially explain the proof failure.
Note that Danfy cannot guarantee that the counterexample it reports provably violates the assertion it was generated for (see 3)
The counterexample takes the form of assumptions that can be inserted into the code to describe the potential conditions under which the given assertion is violated.
This output should be inspected manually and treated as a hint.
In this section, we describe techniques to apply in the case when verification is slower than expected, does not terminate, or times out.
Additional detail is available in the verification optimization guide.
Assuming false is an empirical way to short-circuit the verifier and usually stop verification at a given point,4 and since the final compilation steps do not accept this command, it is safe to use it during development.
Another similar command, assert false;, would also short-circuit the verifier, but it would still make the verifier try to prove false, which can also lead to timeouts.
Thus, let us say a program of this shape takes forever to verify.
method NotTerminating(b: bool) {
assert X;
if b {
assert Y;
} else {
assert Z;
assert P;
}
}What we can first do is add an assume false at the beginning of the method:
method NotTerminating() {
assume false; // Will never compile, but everything verifies instantly
assert X;
if b {
assert Y;
} else {
assert Z;
assert P;
}
assert W;
}This verifies instantly. This gives us a strategy to bisect, or do binary search to find the assertion that slows everything down.
Now, we move the assume false; below the next assertion:
method NotTerminating() {
assert X;
assume false;
if b {
assert Y;
} else {
assert Z;
assert P;
}
assert W;
}If verification is slow again, we can use techniques seen before to decompose the assertion and find which component is slow to prove.
If verification is fast, that's the sign that X is probably not the problem,. We now move the assume false; after the if/then block:
method NotTerminating() {
assert X;
if b {
assert Y;
} else {
assert Z;
assert P;
}
assume false;
assert W;
}Now, if verification is fast, we know that assert W; is the problem. If it is slow, we know that one of the two branches of the if is the problem.
The next step is to put an assume false; at the end of the then branch, and an assume false at the beginning of the else branch:
method NotTerminating() {
assert X;
if b {
assert Y;
assume false;
} else {
assume false;
assert Z;
assert P;
}
assert W;
}Now, if verification is slow, it means that assert Y; is the problem.
If verification is fast, it means that the problem lies in the else branch.
One trick to ensure we measure the verification time of the else branch and not the then branch is to move the first assume false; to the top of the then branch, along with a comment indicating that we are short-circuiting it for now.
Then, we can move the second assume false; down and identify which of the two assertions makes the verifier slow.
method NotTerminating() {
assert X;
if b {
assume false; // Short-circuit because this branch is verified anyway
assert Y;
} else {
assert Z;
assume false;
assert P;
}
assert W;
}If verification is fast, which of the two assertions assert Z; or assert P; causes the slowdown?5
We now hope you know enough of assume false; to locate assertions that make verification slow.
Next, we will describe some other strategies at the assertion level to figure out what happens and perhaps fix it.
If an assertion assert X; is slow, it is possible that calling a lemma or invoking other assertions can help to prove it: The postcondition of this lemma, or the added assertions, could help the dafny verifier figure out faster how to prove the result.
assert SOMETHING_HELPING_TO_PROVE_LEMMA_PRECONDITION;
LEMMA();
assert X;
...
lemma ()
requires LEMMA_PRECONDITION
ensures X { ... }However, this approach has the problem that it exposes the asserted expressions and lemma postconditions not only for the assertion we want to prove faster,
but also for every assertion that appears afterwards. This can result in slowdowns6.
A good practice consists of wrapping the intermediate verification steps in an assert ... by {}, like this:
assert X by {
assert SOMETHING_HELPING_TO_PROVE_LEMMA_PRECONDITION;
LEMMA();
}Now, only X is available for the dafny verifier to prove the rest of the method.
Another way to prevent assertions or preconditions from cluttering the verifier6 is to label and reveal them. Labeling an assertion has the effect of "hiding" its result, until there is a "reveal" calling that label.
The example of the previous section could be written like this.
assert p: SOMETHING_HELPING_TO_PROVE_LEMMA_PRECONDITION;
// p is not available here.
assert X by {
reveal p;
LEMMA();
}Similarly, if a precondition is only needed to prove a specific result in a method, one can label and reveal the precondition, like this:
method Slow(i: int, j: int)
requires greater: i > j {
assert i >= j by {
reveal greater;
}
}Labelled assert statements are available both in expressions and statements. Assertion labels are not accessible outside of the block which the assert statement is in. If you need to access an assertion label outside of the enclosing expression or statement, you need to lift the labelled statement at the right place manually, e.g. rewrite
ghost predicate P(i: int)
method TestMethod(x: bool)
requires r: x <==> P(1)
{
if x {
assert a: P(1) by { reveal r; }
}
assert x ==> P(1) by { reveal a; } // Error, a is not accessible
}to
ghost predicate P(i: int)
method TestMethod(x: bool)
requires r: x <==> P(1)
{
assert a: x ==> P(1) by {
if x {
assert P(1) by { reveal r; } // Proved without revealing the precondition
}
}
assert x ==> P(1) by { reveal a; } // Now a is accessible
}To lift assertions, please refer to the techniques described in Verification Debugging.
Functions are normally used for specifications, but their functional syntax is sometimes also desirable to write application code.
However, doing so naively results in the body of a function method Fun() be available for every caller, which can cause the verifier to time out or get extremely slow6.
A solution for that is to add the attribute {:opaque} right between function method and Fun(), and use reveal Fun(); in the calling functions or methods when needed.
Bitvectors and natural integers are very similar, but they are not treated the same by the dafny verifier. As such, conversion from bv8 to an int and vice-versa is not straightforward, and can result in slowdowns.
There are two solutions to this for now. First, one can define a subset type instead of using the built-in type bv8:
type byte = x | 0 <= x < 256One of the problems of this approach is that additions, subtractions and multiplications do not enforce the result to be in the same bounds, so it would have to be checked, and possibly truncated with modulos. For example:
type byte = x | 0 <= x < 256
method m() {
var a: byte := 250;
var b: byte := 200;
var c := b - a; // inferred to be an 'int', its value will be 50.
var d := a + b; // inferred to be an 'int', its value will be 450.
var e := (a + b) % 256; // still inferred to be an 'int'...
var f: byte := (a + b) % 256; // OK
}A better solution consists of creating a newtype that will have the ability to check bounds of arithmetic expressions, and can actually be compiled to bitvectors as well.
newtype {:nativeType "short"} byte = x | 0 <= x < 256
method m() {
var a: byte := 250;
var b: byte := 200;
var c := b - a; // OK, inferred to be a byte
var d := a + b; // Error: cannot prove that the result of a + b is of type `byte`.
var f := ((a as int + b as int) % 256) as byte; // OK
}One might consider refactoring this code into separate functions if used over and over.
In the case of nested loops, the verifier might timeout sometimes because of inadequate or too much available information6. One way to mitigate this problem, when it happens, is to isolate the inner loop by refactoring it into a separate method, with suitable pre and postconditions that will usually assume and prove the invariant again. For example,
while X
invariant Y
{
while X'
invariant Y'
{
}
}could be refactored as this:
`while X
invariant Y
{
innerLoop();
}
...
method innerLoop()
require Y'
ensures Y'In the next section, when everything can be proven in a timely manner, we explain another strategy to decrease proof time by parallelizing it if needed, and making the verifier focus on certain parts.
To understand how to control verification,
it is first useful to understand how dafny verifies functions and methods.
For every method (or function, constructor, etc.), dafny extracts assertions.
Assertions can roughly be sorted into two kinds: Well-formedness and correctness.
-
Well-formedness assertions: All the implicit requirements of native operation calls (such as indexing and asserting that divisiors are nonzero),
requiresclauses of function calls, explicit assertion expressions anddecreasesclauses at function call sites generate well-formedness assertions.
An expression is said to be well-formed in a context if all well-formedness assertions can be proven in that context. -
Correctness assertions: All remaining assertions and clauses
For example, given the following statements:
if b {
assert a*a != 0;
}
c := (assert b ==> a != 0; if b then 3/a else f(a));
assert c != 5/a;Dafny performs the following checks:
var c: int;
if b {
assert a*a != 0; // Correctness
}
assert b ==> a != 0; // Well-formedness
if b {
assert a != 0; // Well-formedness
} else {
assert f.requires(a); // Well-formedness
}
c := if b then 3/a else f(a);
assert a != 0; // Well-formedness
assert c != 5/a; // CorrectnessWell-formedness is proved at the same time as correctness, except for well-formedness of requires and ensures clauses which is proved separately from the well-formedness and correctness of the rest of the method/function. For the rest of this section, we don't differentiate between well-formedness assertions and correctness assertions.
We can also classify the assertions extracted by Dafny in a few categories:
Integer assertions:
- Every division yields an assertion that the divisor is never zero.
- Every bounded number operation yields an assertion that the result will be within the same bounds (no overflow, no underflows).
- Every conversion yields an assertion that conversion is compatible.
- Every bitvector shift yields an assertion that the shift amount is never negative, and that the shift amount is within the width of the value.
Object assertions:
- Every object property access yields an assertion that the object is not null.
- Every assignment
o.f := E;yields an assertion thatois among the set of objects of themodifiesclause of the enclosing loop or method. - Every read
o.fyields an assertion thatois among the set of objects of thereadsclause of the enclosing function or predicate. - Every array access
a[x]yields the assertion that0 <= x < a.Length. - Every sequence access
a[x]yields an assertion, that0 <= x < |a|, because sequences are never null. - Every datatype update expression and datatype destruction yields an assertion that the object has the given property.
- Every method overriding a
traityields an assertion that any postcondition it provides implies the postcondition of its parent trait, and an assertion that any precondition it provides is implied by the precondition of its parent trait.
Other assertions:
- Every value whose type is assigned to a subset type yields an assertion that it satisfies the subset type constraint.
- Every non-empty subset type yields an assertion that its witness satisfies the constraint.
- Every Assign-such-that operator
x :| P(x)yields an assertion thatexists x :: P(x). In casex :| P(x); Body(x)appears in an expression andxis non-ghost, it also yieldsforall x, y | P(x) && P(y) :: Body(x) == Body(y). - Every recursive function yields an assertion that it terminates.
- Every match expression or alternative if statement yields an assertion that all cases are covered.
- Every call to a function or method with a
requiresclause yields one assertion per requires clause7 (special cases such as sequence indexing come with a specialrequiresclause that the index is within bounds).
Specification assertions:
- Any explicit
assertstatement is an assertion7. - A consecutive pair of lines in a
calcstatement forms an assertion that the expressions are related according to the common operator. - Every
ensuresclause yields an assertion at the end of the method and on every return, and onforallstatements. - Every
invariantclause yields an assertion that it holds before the loop and an assertion that it holds at the end of the loop. - Every
decreasesclause yields an assertion at either a call site or at the end of a while loop. - Every
yield ensuresclause on an iterator yields assertions that the clause holds at every yielding point. - Every
yield requiresclause on an iterator yields assertions that the clause holds at every point when the iterator is called.
It is useful to mentally visualize all these assertions as a list that roughly follows the order in the code,
except for ensures or decreases that generate assertions that seem earlier in the code but, for verification purposes, would be placed later.
In this list, each assertion depends on other assertions, statements and expressions that appear earlier in the control flow8.
The fundamental unit of verification in dafny is an assertion batch, which consists of one or more assertions from this "list", along with all the remaining assertions turned into assumptions. To reduce overhead, by default dafny collects all the assertions in the body of a given method into a single assertion batch that it sends to the verifier, which tries to prove it correct.
- If the verifier says it is correct,3 it means that all the assertions hold.
- If the verifier returns a counterexample, this counterexample is used to determine both the failing assertion and the failing path.
In order to retrieve additional failing assertions,
dafnywill again query the verifier after turning previously failed assertions into assumptions.9 10 - If the verifier returns
unknownor times out, or even preemptively for difficult assertions or to reduce the chance that the verifier will ‘be confused’ by the many assertions in a large batch,dafnymay partition the assertions into smaller batches11. An extreme case is the use of the/vcsSplitOnEveryAssertcommand-line option or the{:isolate_assertions}attribute, which causesdafnyto make one batch for each assertion.
When Dafny verifies a symbol, such as a method, a function or a constant with a subset type, that verification may contain multiple assertions. A symbol is generally verified the fastest when all assertions it in are verified together, in what we call a single 'assertion batch'. However, is it possible to split verification of a symbol into multiple batches, and doing so makes the individual batches simpler, which can lead to less brittle verification behavior. Dafny contains several attributes that allow you to customize how verification is split into batches.
Firstly, you can instruct Dafny to verify individual assertions in separate batches. You can place the {:isolate} attribute on a single assertion to place it in a separate batch, or you can place {:isolate_assertions} on a symbol, such as a function or method declaration, to place all assertions in it into separate batches. The CLI option --isolate-assertions will place all assertions into separate batches for all symbols. {:isolate} can be used on assert, return and continue statements. When placed on a return statement, it will verify the postconditions for all paths leading to that return in a separate batch. When placed on a continue, it will verify the loop invariants for all paths leading to that continue in a separate batch.
Given an assertion that is placed into a separate batch, you can then further simplify the verification of this assertion by placing each control flow path that leads to this assertion into a separate batch. You can do this using the attribute {:isolate "paths"}.
13.7.4. Command-line options and other attributes to control verification {#sec-command-line-options-and-attributes-for-verification}
There are many great options that control various aspects of verifying dafny programs. Here we mention only a few:
- Control of output:
/dprint,/rprint,/stats,/compileVerbose - Whether to print warnings:
/proverWarnings - Control of time:
/timeLimit - Control of resources:
/rLimitand{:rlimit} - Control of the prover used:
/prover - Control of how many times to unroll functions:
{:fuel}
You can search for them in this file as some of them are still documented in raw text format.
When Dafny successfully verifies a particular definition, it can ask the solver for information about what parts of the program were actually used in completing the proof. The program components that can potentially form part of a proof include:
assertstatements (and the implicit assumption that they hold in subsequent code),- implicit assertions (such as array or sequence bounds checks),
assumestatements,ensuresclauses,requiresclauses,- function definitions,
- method calls, and
- assignment statements.
Understanding what portions of the program the proof depended on can help identify mistakes, and to better understand the structure of your proof (which can help when optimizing it, among other things). In particular, there are two key dependency structures that tend to indicate mistakes, both focused on what parts of the program were not included in the proof.
-
Redundant assumptions. In some cases, a proof can be completed without the need of certain
assumestatements orrequiresclauses. This situation might represent a mistake, and when the mistake is corrected those program elements may become required. However, they may also simply be redundant, and the program will become simpler if they're removed. Dafny will report assumptions of this form when verifying with the flag--warn-redundant-assumptions. Note thatassertstatements may be warned about, as well, indicating that the fact proved by the assertion wasn't needed to prove anything else in the program. -
Contradictory assumptions. If the combination of all assumptions in scope at a particular program point is contradictory, anything can be proved at that point. This indicates the serious situation that, unless done on purpose in a proof by contradiction, your proof may be entirely vacuous. It therefore may not say what you intended, giving you a false sense of confidence. The
--warn-contradictory-assumptionsflag instructs Dafny to warn about any assertion that was proved through the use of contradictions between assumptions. If a particularassertstatement is part of an intentional proof by contradiction, annotating it with the{:contradiction}attribute will silence this warning.
These options can be specified in dfyconfig.toml, and this is typically the most convenient way to use them with the IDE.
More detailed information is available using either the --log-format text or --verification-coverage-report option to dafny verify. The former will
include a list of proof dependencies (including source location and
description) alongside every assertion batch in the generated log
whenever one of the two warning options above is also included. The
latter will produce a highlighted HTML version of your source code, in
the same format used by dafny test --coverage-report
and dafny generate-tests --verification-coverage-report,
indicating which parts of the program were used, not used, or partly
used in the verification of the entire program.
When evolving a Dafny codebase, it can sometimes occur that a proof obligation succeeds at first only for the prover to time out or report a potential error after minor, valid changes. We refer to such a proof obligation as brittle. This is ultimately due to decidability limitations in the form of automated reasoning that Dafny uses. The Z3 SMT solver that Dafny depends on attempts to efficiently search for proofs, but does so using both incomplete heuristics and a degree of randomness, with the result that it can sometimes fail to find a proof even when one exists (or continue searching forever).
Dafny provides some features to mitigate this issue, primarily focused on early detection. The philosophy is that, if Dafny programmers are alerted to proofs that show early signs of brittleness, before they are obviously so, they can refactor the proofs to make them less brittle before further development becomes difficult.
The mechanism for early detection focuses on measuring the resources used to discharge a proof obligation (either using duration or a more deterministic "resource count" metric available from Z3). Dafny can re-run a given proof attempt multiple times after automatically making minor changes to the structure of the input or to the random choices made by the solver. If the resources used during these attempts (or the ability to find a proof at all) vary widely, we use this as a proxy metric indicating that the proof may be brittle.
To measure the brittleness of your proofs, start by using the dafny measure-complexity command with the --iterations N flag to instruct
Dafny to attempt each proof goal N times, using a different random
seed each time. The random seed used for each attempt is derived from
the global random seed S specified with -randomSeed:S, which
defaults to 0. The random seed affects the structure of the SMT
queries sent to the solver, changing the ordering of SMT commands, the
variable names used, and the random seed the solver itself uses when
making decisions that can be arbitrary.
For most use cases, it also makes sense to specify the
--log-format csv flag, to log verification cost statistics to a
CSV file. By default, the resulting CSV files will be created in the
TestResults folder of the current directory.
Once Dafny has completed, the
dafny-reportgenerator
tool is a convenient way to process the output. It allows you to specify
several limits on statistics computed from the elapsed time or solver
resource use of each proof goal, returning an error code when it detects
violations of these limits. You can find documentation on the full set
of options for dafny-reportgenerator in its
README.md
file.
In general, we recommend something like the following:
dafny-reportgenerator --max-resource-cv-pct 10 TestResults/*.csvThis bounds the coefficient of variation of the solver resource count at 10% (0.10). We recommend a limit of less than 20%, perhaps even as low as 5%. However, when beginning to analyze a new project, it may be necessary to set limits as high as a few hundred percent and incrementally ratchet down the limit over time.
When first analyzing proof brittleness, you may also find that certain proof
goals succeed on some iterations and fail on others. If your aim is
first to ensure that brittleness doesn't worsen and then to start
reducing it, integrating dafny-reportgenerator into CI and using the
--allow-different-outcomes flag may be appropriate. Then, once you've
improved brittleness sufficiently, you can likely remove that flag (and
likely have significantly lower limits on other metrics).
Reducing proof brittleness is typically closely related to improving performance overall. As such, techniques for debugging slow verification are typically useful for debugging brittle proofs, as well. See also the verification optimization guide.
The dafny tool can compile a Dafny program to one of several target languages. Details and idiosyncrasies of each
of these are described in the following subsections. In general note the following:
- The compiled code originating from
dafnycan be combined with other source and binary code, but only thedafny-originated code is verified. - Output file or folder names can be set using
--output. - Code generated by
dafnyrequires a Dafny-specific runtime library. By default the runtime is included in the generated code. However fordafny translateit is not included by default and must be explicitly requested using--include-runtime. All runtime libraries are part of the Binary (./DafnyRuntime.*) and Source (./Source/DafnyRuntime/DafnyRuntime.*) releases. - Names in Dafny are written out as names in the target language. In some cases this can result in naming conflicts. Thus if a Dafny program is intended to be compiled to a target language X, you should avoid using Dafny identifiers that are not legal identifiers in X or that conflict with reserved words in X.
To be compilable to an executable program, a Dafny program must contain a Main entry point, as described here.
Dafny includes several built-in types such as tuples, arrays, arrows (functions), and the nat subset type.
The supporting target language code for these declarations could be emitted on-demand,
but these could then become multiple definitions of the same symbols when compiling multiple components separately.
Instead, all such built-ins up to a pre-configured maximum size are included in most of the runtime libraries.
This means that when compiling to certain target languages, the use of such built-ins above these maximum sizes,
such as tuples with more than 20 elements, is not supported.
See the Supported features by target language table
for the details on these limits.
A Dafny declaration can be marked with the {:extern} attribute to
indicate that it refers to an external definition that is already
present in the language that the Dafny code will be compiled to (or will
be present by the time the final target-language program is compiled or
run).
Because the {:extern} attribute controls interaction with code written
in one of many languages, it has some language-specific behavior,
documented in the following sections. However, some aspects are
target-language independent and documented here.
The attribute can also take several forms, each defining a different
relationship between a Dafny name and a target language name. In the
form {:extern}, the name of the external definition is
assumed to be the name of the Dafny declaration after some
target-specific name mangling. However, because naming conventions (and
the set of allowed identifiers) vary between languages, Dafny allows
additional forms for the {:extern} attribute.
The form {:extern <s1>} instructs dafny to compile references to most
declarations using the name s1 instead of the Dafny name. For abstract
types, however, s1 is sometimes used as a hint as
to how to declare that type when compiling. This hint is interpreted
differently by each compiler.
Finally, the form {:extern <s1>, <s2>} instructs dafny to use s2 as
the direct name of the declaration. dafny will typically use a
combination of s1 and s2, such as s1.s2, to reference the
declaration. It may also be the case that one of the arguments is simply
ignored, depending on the target language.
The recommended style is to prefer {:extern} when possible, and use
similar names across languages. This is usually feasible because
existing external code is expected to have the same interface as the
code that dafny would generate for a declaration of that form. Because
many Dafny types compile down to custom types defined in the Dafny
runtime library, it's typically necessary to write wrappers by hand that
encapsulate existing external code using a compatible interface, and
those wrappers can have names chosen for compatibility. For example,
retrieving the list of command line arguments when compiling to C#
requires a wrapper such as the following:
using icharseq = Dafny.ISequence<char>;
using charseq = Dafny.Sequence<char>;
namespace Externs_Compile {
public partial class __default {
public static Dafny.ISequence<icharseq> GetCommandLineArgs() {
var dafnyArgs = Environment
.GetCommandLineArgs()
.Select(charseq.FromString);
return Dafny.Sequence<icharseq>.FromArray(dafnyArgs.ToArray());
}
}This serves as an example of implementing an extern,
but was only necessary to retrieve command line arguments historically,
as dafny now supports capturing these arguments via a main method
that accepts a seq<string> (see the section on the Main method).
Note that dafny does not check the arguments to {:extern}, so it is
the user's responsibility to ensure that the provided names result in
code that is well-formed in the target language.
Also note that the interface the external code needs to implement
may be affected by compilation flags. In this case, if --unicode-char:true
is provided, dafny will compile its char type to the Dafny.Rune
C# type instead, so the references to the C# type char above
would need to be changed accordingly. The reference to charseq.FromString
would in turn need to be changed to charseq.UnicodeFromString to
return the correct type.
Most declarations, including those for modules, classes, traits, member
variables, constructors, methods, function methods, and abstract types,
can be marked with {:extern}.
Marking a module with {:extern} indicates that the declarations
contained within can be found within the given module, namespace, package, or
similar construct within the target language. Some members of the Dafny
module may contain definitions, in which case code for those definitions
will be generated. Whether this results in valid target code may depend
on some target language support for something resembling "partial"
modules, where different subsets of the contents are defined in
different places.
The story for classes is similar. Code for a class will be generated
if any of its members are not {:extern}. Depending on the target
language, making either all or none of the members {:extern} may be
the only options that result in valid target code. Traits with
{:extern} can refer to existing traits or interfaces in the target
language, or can refer to the interfaces of existing classes.
Member variables marked with {:extern} refer to fields or properties
in existing target-language code. Constructors, methods, and functions
refer to the equivalent concepts in the target language. They
can have contracts, which are then assumed to hold for the existing
target-language code. They can also have bodies, but the bodies will not
be compiled in the presence of the {:extern} attribute. Bodies can
still be used for reasoning, however, so may be valuable in some cases,
especially for function methods.
Types marked with {:extern} must be opaque. The name argument, if any,
usually refers to the type name in the target language, but some
compilers treat it differently.
Detailed description of the dafny build and dafny run commands and
the --input option (needed when dafny run has more than one input file)
is contained in the section on command-line structure.
To enable easily customising runtime behavior across an entire Dafny program, Dafny has placeholder modules. Here follows an example:
replaceable module Foo {
method Bar() returns (i: int)
ensures i >= 2
}
method Main() {
var x := Foo.Bar();
print x;
}
// At this point, the program can be verified but not run.
module ConcreteFoo replaces Foo {
method Bar() returns (i: int) {
return 3; // Main will print 3.
}
}
// ConcreteFoo can be swapped out for different replacements of Foo, to customize runtime behavior.When replacing a replaceable module, the same rules apply as when refining an abstract module. However, unlike an abstract module, a placeholder module can be used as if it is a concrete module. When executing code, using for example dafny run or dafny translate, any program that contains a placeholder module must also contain a replacement of this placeholder. When using dafny verify, placeholder modules do not have to be replaced.
Replaceable modules are particularly useful for defining behavior that depends on which target language Dafny is translated to.
For a simple Dafny-only program, the translation step converts a A.dfy file into A.cs;
the build step then produces a A.dll, which can be used as a library or as an executable (run using dotnet A.dll).
It is also possible to run the dafny files as part of a csproj project, with these steps:
- create a dotnet project file with the command
dotnet new console - delete the
Program.csfile - build the dafny program:
dafny build A.dfy - run the built program
dotnet A.dll
The last two steps can be combined:
dafny run A.dfy
Note that all input .dfy files and any needed runtime library code are combined into a single .cs file,
which is then compiled by dotnet to a .dll.
Examples of how to integrate C# libraries and source code with Dafny source code are contained in this separate document.
The Dafny-to-Java compiler translation phase writes out the translated files of a file A.dfy
to a directory A-java.
The build phase writes out a library or executable jar file.
The --output option (-out in the legacy CLI) can be used to choose a
different jar file path and name and correspondingly different directory for .java and .class files.
The compiler produces a single wrapper method that then calls classes in
relevant other .java files. Because Java files must be named consistent
with the class they contain, but Dafny files do not, there may be no relation
between the Java file names and the Dafny file names.
However, the wrapper class that contains the Java main method is named for
the first .dfy file on the command-line.
The step of compiling Java files (using javac) requires the Dafny runtime library.
That library is automatically included if dafny is doing the compilation,
but not if dafny is only doing translation.
Examples of how to integrate Java source code and libraries with Dafny source are contained in this separate document.
The Dafny-to-Javascript compiler translates all the given .dfy files into a single .js file,
which can then be run using node. (Javascript has no compilation step).
The build and run steps are simply
dafny build --target:js A.dfynode A.js
Or, in one step,
dafny run A.dfy
Examples of how to integrate Javascript libraries and source code with Dafny source are contained in this separate document.
The Dafny-to-Go compiler translates all the given .dfy files into a single
.go file in A-go/src/A.go; the output folder can be specified with the
-out option. For an input file A.dfy the default output folder is A-go.
Then, Dafny compiles this program and creates an A.exe executable in the same folder as A.dfy.
Some system runtime code is also placed in A-go/src.
The build and run steps are
dafny build --target:go A.dfy./A
The uncompiled code can be compiled and run by go itself using
(cd A-go; GO111MODULE=auto GOPATH=`pwd` go run src/A.go)
The one-step process is
dafny run --target:go A.dfy
The GO111MODULE variable is used because Dafny translates to pre-module Go code.
When the implementation changes to current Go, the above command-line will
change, though the ./A alternative will still be supported.
Examples of how to integrate Go source code and libraries with Dafny source are contained in this separate document.
The Dafny-to-Python compiler is still under development. However, simple
Dafny programs can be built and run as follows. The Dafny-to-Python
compiler translates the .dfy files into a single .py file along with
supporting runtime library code, all placed in the output location
(A-py for an input file A.dfy, by default).
The build and run steps are
dafny build --target:py A.dfypython A-py/A.py
In one step:
dafny run --target:py A.dfy
Examples of how to integrate Python libraries and source code with Dafny source are contained in this separate document.
The C++ backend was written assuming that it would primarily support writing C/C++ style code in Dafny, which leads to some limitations in the current implementation.
- The C++ compiler does not support BigIntegers, so do not use
int, or raw instances ofarr.Length, or sequence length, etc. in executable code. You can however, usearr.Length as uint64if you can prove your array is an appropriate size. The compiler will report inappropriate integer use. - The C++ compiler does not support advanced Dafny features like traits or coinductive types.
- There is very limited support for higher order functions even for array initialization. Use
extern definitions like newArrayFill (see
extern.dfy) or
similar. See also the example in [
functions.dfy] (https://github.com/dafny-lang/dafny/blob/master/Test/c++/functions.dfy). - The current backend also assumes the use of C++17 in order to cleanly and performantly implement datatypes.
Some Dafny features are not supported by every target language. The table below shows which features are supported by each backend. An empty cell indicates that a feature is not supported, while an X indicates that it is.
{% include_relative Features.md %}
There are many command-line options to the dafny tool.
The most current documentation of the options is within the tool itself,
using the -? or --help or -h options.
Remember that options are typically stated with either a leading --.
Legacy options begin with either '-' or '/'; however they are being
migrated to the POSIX-compliant -- form as needed.
These options emit general information about commands, options and attributes. When present, the dafny program will terminates after emitting the requested information but without processing any files.
-
--help,-h- shows the various commands (which have help information under them asdafny <command> -h -
--version- show the version of the build
Legacy options:
-
-?- print out the legacy list of command-line options and terminate. All of these options are also described in this and the following sections. -
-attrHelp- print out the current list of supported attribute declarations and terminate. -
-env:<n>- print the command-line arguments supplied to the program. The value of<n>can be one of the following.-
0- never print command-line arguments. -
1(default) - print them to Boogie (.bpl) files and prover logs. -
2- operate like with option1but also print to standard output.
-
-
-wait- wait for the user to pressEnterbefore terminating after a successful execution.
These options control how Dafny processes its input.
-
-stdin- read standard input and treat it as Dafny source code, instead of reading from a file. -
--library:<files>- treat the given files as library code, namely, skip these files (and any files recursively included) during verification; the value may be a comma-separated-list of files or folders; folders are expanded into a list of all .dfy files contained, recursively, in those folders -
--prelude:<file>(was-dprelude) - select an alternative Dafny prelude file. This file contains Boogie definitions (including many axioms) required by the translator from Dafny to Boogie. Using an alternative prelude is primarily useful if you're extending the Dafny language or changing how Dafny constructs are modeled. The default prelude is here.
Dafny has a plugin capability. A plugin has access to an AST of the dafny input files after all parsing and resolution are performed (but not verification) and also to the command-line options.
This facility is still experimental and very much in flux, particularly
the form of the AST. The best guides to writing a new plugin are
(a) the documentation in the section of this manual on plugins
and (b) example plugins in the
src/Tools folder of the dafny-lang/compiler-bootstrap repo.
The value of the option --plugin is a path to a dotnet dll that contains
the compiled plugin.
These options instruct Dafny to print various information about your program during processing, including variations of the original source code (which can be helpful for debugging).
-
--use-basename-for-filename- when enabled, just the filename without the directory path is used in error messages; this make error message shorter and not tied to the local environment (which is a help in testing) -
--output,-o- location of output files [translate, build] -
--show-snippets- include with an error message some of the source code text in the neighborhood of the error; the error location (file, line, column) is always given -
--solver-log <file>- [verification only] the file in which to place the SMT text sent to the solver -
--log-format <configuration>- [verification only] (was-verificationLogger:<configuration string>) log verification results to the given test result logger. The currently supported loggers aretrx,csv, andtext. These are the XML-based formats commonly used for test results for .NET languages, a custom CSV schema, and a textual format meant for human consumption, respectively. You can provide configuration using the same string format as when using the--loggeroption for dotnet test, such as:-verificationLogger:trx;LogFileName=<...>The exact mapping of verification concepts to these formats is experimental and subject to change!
The
trxandcsvloggers automatically choose an output file name by default, and print the name of this file to the console. Thetextlogger prints its output to the console by default, but can send output to a file given theLogFileNameoption.The
textlogger also includes a more detailed breakdown of what assertions appear in each assertion batch. When combined with the-vcsSplitOnEveryAssertoption, it will provide approximate time and resource use costs for each assertion, allowing identification of especially expensive assertions.
Legacy options:
-
-stats- print various statistics about the Dafny files supplied on the command line. The statistics include the number of total functions, recursive functions, total methods, ghost methods, classes, and modules. They also include the maximum call graph width and the maximum module height. -
-dprint:<file>- print the Dafny program after parsing (use-for<file>to print to the console). -
-rprint:<file>- print the Dafny program after type resolution (use-for<file>to print to the console). -
-printMode:<Everything|DllEmbed|NoIncludes|NoGhost>- select what to include in the output requested by-dprintor-rprint. The argument can be one of the following.-
Everything(default) - include everything. -
DllEmbed- print the source that will be included in a compiled DLL. -
NoIncludes- disable printing of methods incorporated via the include mechanism that have the{:verify false}attribute, as well as datatypes and fields included from other files. -
NoGhost- disables printing of functions, ghost methods, and proof statements in implementation methods. Also disable anythingNoIncludesdisables.
-
-
-printIncludes:<None|Immediate|Transitive>- select what information from included files to incorporate into the output selected by-dprintor-rprint. The argument can be one of the following.-
None(default) - don't print anything from included files. -
Immediate- print files directly included by files specified on the command line. Exit after printing. -
Transitive- print files transitively included by files specified on the command line. Exit after printing.
-
-
-view:<view1, view2>- this option limits what is printed by /rprint for a module to the names that are part of the given export set; the option argument is a comma-separated list of fully-qualified export set names. -
-funcCallGraph- print out the function call graph. Each line has the formatfunc,mod=callee*, wherefuncis the name of a function,modis the name of its containing module, andcallee*is a space-separated list of the functions thatfunccalls. -
--show-snippets(was-showSnippets:<n>) - show a source code snippet for each Dafny message. The legacy option was-showSnippetswith values 0 and 1 for false and true. -
-printTooltips- dump additional positional information (displayed as mouse-over tooltips by LSP clients) to standard output asInfomessages. -
-pmtrace- print debugging information from the pattern-match compiler. -
-titrace- print debugging information during the type inference process. -
-diagnosticsFormat:<text|json>- control how to report errors, warnings, and info messages.<fmt>may be one of the following:-
text(default): Report diagnostics in human-readable format. -
json: Report diagnostics in JSON format, one object per diagnostic, one diagnostic per line. Info-level messages are only included with-printTooltips. End positions are only included with-showSnippets:1. Diagnostics are the following format (but without newlines):{ "location": { "filename": "xyz.dfy", "range": { // Start and (optional) end of diagnostic "start": { "pos": 83, // 0-based character offset in input "line": 6, // 1-based line number "character": 0 // 0-based column number }, "end": { "pos": 86, "line": 6, "character": 3 } } }, "severity": 2, // 1: error; 2: warning; 4: info "message": "module-level const declarations are always non-instance ...", "source": "Parser", "relatedInformation": [ // Additional messages, if any { "location": { ... }, // Like above "message": "...", } ] }
-
These options allow some Dafny language features to be enabled or disabled. Some of these options exist for backward compatibility with older versions of Dafny.
-
--default-function-opacity:<transparent|autoRevealDependencies|opaque>- Change the default opacity of functions.transparent(default) means functions are transparent, can be manually made opaque and then revealed.autoRevealDependenciesmakes all functions not explicitly labelled as opaque to be opaque but reveals them automatically in scopes which do not have{:autoRevealDependencies false}.opaquemeans functions are always opaque so the opaque keyword is not needed, and functions must be revealed everywhere needed for a proof.
-
--function-syntax(value '3' or '4') - permits a choice of using the Dafny 3 syntax (functionandfunction method) or the Dafny 4 syntax (ghost functionandfunction) -
--quantifier-syntax(value '3' or '4') - permits a choice between the Dafny 3 and Dafny 4 syntax for quantifiers -
--unicode-char- if false, thechartype represents any UTF-16 code unit, that is, any 16-bit value, including surrogate code points and allows\uXXXXescapes in string and character literals. If true,charrepresents any Unicode scalar value, that is, any Unicode code point excluding surrogates and allows\U{X..X}escapes in string and character literals. The default is false for Dafny version 3 and true for version 4. The legacy option was-unicodeChar:<n>with values 0 and 1 for false and true above.
Legacy options:
-
-noIncludes- ignoreincludedirectives in the program. -
-noExterns- ignoreexternattributes in the program.
-
--function-syntax:<version>(was-functionSyntax:<version>) - select what function syntax to recognize. The syntax for functions is changing from Dafny version 3 to version 4. This switch gives early access to the new syntax, and also provides a mode to help with migration. The valid arguments include the following.-
3(default) - compiled functions are writtenfunction methodandpredicate method. Ghost functions are writtenfunctionandpredicate. -
4- compiled functions are writtenfunctionandpredicate. Ghost functions are writtenghost functionandghost predicate. -
migration3to4- compiled functions are writtenfunction methodandpredicate method. Ghost functions are writtenghost functionandghost predicate. To migrate from version 3 to version 4, use this flag on your version 3 program to flag all occurrences offunctionandpredicateas parsing errors. These are ghost functions, so change those into the new syntaxghost functionandghost predicate. Then, start using
-functionSyntax:4. This will flag all occurrences offunction methodandpredicate methodas parsing errors. So, change those to justfunctionandpredicate. As a result, your program will use version 4 syntax and have the same meaning as your previous version 3 program. -
experimentalDefaultGhost- likemigration3to4, but allowfunctionandpredicateas alternatives to declaring ghost functions and predicates, respectively -
experimentalDefaultCompiled- likemigration3to4, but allowfunctionandpredicateas alternatives to declaring compiled functions and predicates, respectively -
experimentalPredicateAlwaysGhost- compiled functions are writtenfunction. Ghost functions are writtenghost function. Predicates are always ghost and are writtenpredicate.
This option can also be set locally (at the module level) using the
:optionsattribute: -
module {:options "--function-syntax:4"} M {
predicate CompiledPredicate() { true }
}-
--quantifier-syntax:<version>(was-quantifierSyntax:<version>) - select what quantifier syntax to recognize. The syntax for quantification domains is changing from Dafny version 3 to version 4, more specifically where quantifier ranges (| <Range>) are allowed. This switch gives early access to the new syntax.3(default) - Ranges are only allowed after all quantified variables are declared. (e.g.set x, y | 0 <= x < |s| && y in s[x] && 0 <= y :: y)4- Ranges are allowed after each quantified variable declaration. (e.g.set x | 0 <= x < |s|, y <- s[x] | 0 <= y :: y)
Note that quantifier variable domains (
<- <Domain>) are available in both syntax versions. -
-disableScopes- treat all export sets asexport reveal *to never hide function bodies or type definitions during translation. -
-allowsGlobals- allow the implicit class_defaultto contain fields, instance functions, and instance methods. These class members are declared at the module scope, outside of explicit classes. This command-line option is provided to simplify a transition from the behavior in the language prior to version 1.9.3, from which point onward all functions and methods declared at the module scope are implicitly static and field declarations are not allowed at the module scope.
These options control what warnings Dafny produces, and whether to treat warnings as errors.
-
--warn-as-errors(was-warningsAsErrors) - treat warnings as errors. -
--warn-shadowing(was-warnShadowing) - emit a warning if the name of a declared variable caused another variable to be shadowed. -
--warn-missing-constructor-parentheses- warn if a constructor name in a pattern might be misinterpreted
Legacy options
-
-deprecation:<n>- control warnings about deprecated features. The value of<n>can be any of the following.-
0- don't issue any warnings. -
1(default) - issue warnings. -
2- issue warnings and advise about alternate syntax.
-
These options control how Dafny verifies the input program, including how much it verifies, what techniques it uses to perform verification, and what information it produces about the verification process.
-
--no-verify- turns off verification (for translate, build, run commands) -
--verify-included-files(was-verifyAllModules) - verify modules that come from include directives.By default, Dafny only verifies files explicitly listed on the command line: if
a.dfyincludesb.dfy, a call toDafny a.dfywill detect and report verification errors froma.dfybut not fromb.dfy.With this option, Dafny will instead verify everything: all input modules and all their transitive dependencies. This way
Dafny a.dfywill verifya.dfyand all files that it includes (hereb.dfy), as well all files that these files include, etc.Running Dafny with this option on the file containing your main result is a good way to ensure that all its dependencies verify.
-
--track-print-effects- If true, a compiled method, constructor, or iterator is allowed to have print effects only if it is marked with {{:print}}. (default false) The legacy option was-trackPrintEffects:<n>) with values 0 or 1 for false and true. -
--relax-definite-assignment- control the rules governing definite assignment, the property that every variable is eventually assigned a value before it is used.- if false (default), enforce definite-assignment for all non-yield-parameter variables and fields, regardless of their types
- if false and
--enforce-determinismis true, then also performs checks in the compiler that no nondeterministic statements are used - if true, enforce definite-assignment rules for compiled variables and fields whose types do not support auto-initialization and for ghost variables and fields whose type is possibly empty.
-
--disable-nonlinear-arithmetic(was-noNLarith) - reduce Z3's knowledge of non-linear arithmetic (the operators*,/, and%). Enabling this option will typically require more manual work to complete proofs (by explicitly applying lemmas about non-linear operators), but will also result in more predictable behavior, since Z3 can sometimes get stuck down an unproductive path while attempting to prove things about those operators. (This option will perhaps be replaced by-arithin the future. For now, it takes precedence over-arith.)The behavior of
disable-nonlinear-arithmeticcan be turned on and off on a per-module basis by placing the attribute{:disable-nonlinear-arithmetic}after the module keyword. The attribute optionally takes the valuefalseto enable nonlinear arithmetic. -
--manual-lemma-induction- disables automatic inducntion for lemmas -
--isolate-assertions- verify assertions individually -
--extract-counterexample- if verification fails, report a potential counterexample as a set of assumptions that can be inserted into the code. Note that Danfy cannot guarantee that the counterexample it reports provably violates the assertion or that the assumptions are not mutually inconsistent (see 3), so this output should be inspected manually and treated as a hint.
Controlling the proof engine:
--cores:<n>- sets the number or percent of the available cores to be used for verification--verification-time-limit <seconds>- imposes a time limit on each verification attempt--verification-error-limit <number>- limits the number of verification errors reported (0 is no limit)--resource-limit- states a resource limit (to be used by the backend solver)
Legacy options:
-
-dafnyVerify:<n>[discouraged] - turn verification of the program on or off. The value of<n>can be any of the following.-
0- stop after type checking. -
1- continue on to verification and compilation.
-
-
-separateModuleOutput- output verification results for each module separately, rather than aggregating them after they are all finished. -
-mimicVerificationOf:<dafny version>- letdafnyattempt to mimic the verification behavior of a previous version ofdafny. This can be useful during migration to a newer version ofdafnywhen a Dafny program has proofs, such as methods or lemmas, that are highly variable in the sense that their verification may become slower or fail altogether after logically irrelevant changes are made in the verification input.Accepted versions are:
3.3. Note that falling back on the behavior of version 3.3 turns off features that prevent certain classes of verification variability. -
-noCheating:<n>- control whether certain assumptions are allowed. The value of<n>can be one of the following.-
0(default) - allowassumestatements and free invariants. -
1- treat all assumptions asassertstatements, and drop free invariants.
-
-
-induction:<n>- control the behavior of induction. The value of<n>can be one of the following.-
0- never do induction, not even when attributes request it. -
1- apply induction only when attributes request it. -
2- apply induction as requested (by attributes) and also for heuristically chosen quantifiers. -
3- apply induction as requested, and for heuristically chosen quantifiers and lemmas. -
4(default) - apply induction as requested, and for all lemmas.
-
-
-inductionHeuristic:<n>- control the heuristics used for induction. The value of<n>can be one of the following.-
0- use the least discriminating induction heuristic (that is, lean toward applying induction more often). -
1,2,3,4,5- use an intermediate heuristic, ordered as follows as far as how discriminating they are: 0 < 1 < 2 < (3,4) < 5 < 6. -
6(default) - use the most discriminating induction heuristic.
-
-
-allocated:<n>- specify defaults for where Dafny should assert and assumeallocated(x)for various parametersx, local variablesx, bound variablesx, etc. Lower<n>may require more manualallocated(x)annotations and thus may be more difficult to use. The value of<n>can be one of the following.-
0- never assume or assertallocated(x)by default. -
1- assumeallocated(x)only for non-ghost variables and fields. (These assumptions are free, since non-ghost variables always contain allocated values at run-time.) This option may speed up verification relative to-allocated:2. -
2- assert/assumeallocated(x)on all variables, even bound variables in quantifiers. This option is the easiest to use for code that uses the heap heavily. -
3- (default) make frugal use of heap parameters. -
4- like3but addallocatedantecedents when ranges don't imply allocatedness.
Warning: this option should be chosen consistently across an entire project; it would be unsound to use different defaults for different files or modules within a project. Furthermore, modes
-allocated:0and-allocated:1let functions depend on the allocation state, which is not sound in general. -
-
-noAutoReq- ignoreautoReqattributes, and therefore do not automatically generaterequiresclauses. -
-autoReqPrint:<file>- print the requires clauses that were automatically generated byautoReqto the given<file>. -
-arith:<n>- control how arithmetic is modeled during verification. This is an experimental switch, and its options may change. The value of<n>can be one of the following.-
0- use Boogie/Z3 built-ins for all arithmetic operations. -
1(default) - like0, but introduce symbolic synonyms for*,/, and%, and allow these operators to be used in triggers. -
2- like1, but also introduce symbolic synonyms for+and-. -
3- turn off non-linear arithmetic in the SMT solver. Still use Boogie/Z3 built-in symbols for all arithmetic operations. -
4- like3, but introduce symbolic synonyms for*,/, and%, and allow these operators to be used in triggers. -
5- like4, but also introduce symbolic synonyms for+and-. -
6- like5, and introduce axioms that distribute+over*. -
7- like6, and introduce facts about the associativity of literal arguments over*. -
8- like7, and introduce axioms for the connection between*,/, and%. -
9- like8, and introduce axioms for sign of multiplication. -
10- like9, and introduce axioms for commutativity and associativity of*.
-
-
-autoTriggers:<n>- control automatic generation of{:trigger}annotations. See triggers. The value of<n>can be one of the following.-
0- do not generate{:trigger}annotations for user-level quantifiers. -
1(default) - add a{:trigger}annotation to each user-level quantifier. Existing annotations are preserved.
-
-
-rewriteFocalPredicates:<n>- control rewriting of predicates in the body of prefix lemmas. See the section about nicer extreme proofs. The value of<n>can be one of the following.-
0- don't rewrite predicates in the body of prefix lemmas. -
1(default) - in the body of prefix lemmas, rewrite any use of a focal predicatePtoP#[_k-1].
-
These options control what code gets compiled, what target language is used, how compilation proceeds, and whether the compiled program is immediately executed.
-
--target:<s>or-t:<s>(was-compileTarget:<s>) - set the target programming language for the compiler. The value of<s>can be one of the following.-
cs- C# . Produces a .dll file that can be run usingdotnet. For example,dafny Hello.dfywill produceHello.dllandHello.runtimeconfig.json. The dll can be run usingdotnet Hello.dll. -
go- Go. The default output ofdafny Hello.dfy -compileTarget:gois in theHello-gofolder. It is run usingGOPATH=`pwd`/Hello-go/ GO111MODULE=auto go run Hello-go/src/Hello.go -
js- Javascript. The default output ofdafny Hello.dfy -compileTarget:jsis the fileHello.js, which can be run usingnode Hello.js. (You must havebignumber.jsinstalled.) -
java- Java. The default output ofdafny Hello.dfy -compileTarget:javais in theHello-javafolder. The compiled program can be run usingjava -cp Hello-java:Hello-java/DafnyRuntime.jar Hello. -
py- Python. The default output ofdafny Hello.dfy -compileTarget:pyis in theHello-pyfolder. The compiled program can be run usingpython Hello-py/Hello.py, wherepythonis Python version 3. -
cpp- C++. The default output ofdafny Hello.dfy -compileTarget:cppisHello.exeand other files written to the current folder. The compiled program can be run using./Hello.exe.
-
-
--input <file>- designates files to be include in the compilation in addition to the main file indafny run; these may be non-.dfy files; this option may be specified more than once -
--output:<file>or-o:<file>(was-out:<file>) - set the name to use for compiled code files.
By default, dafny reuses the name of the Dafny file being compiled.
Compilers that generate a single file use the file name as-is (e.g. the
C# backend will generate <file>.dll and optionally <file>.cs with
-spillTargetCode). Compilers that generate multiple files use the file
name as a directory name (e.g. the Java backend will generate files in
directory <file>-java/). Any file extension is ignored, so
-out:<file> is the same as -out:<file>.<ext> if <file> contains no
periods.
--include-runtime- include the runtime library for the target language in the generated artifacts. This is true by default for build and run, but false by default for translate. The legacy option-useRuntimeLibhad the opposite effect: when enabled, the compiled assembly referred to the pre-builtDafnyRuntime.dllin the compiled assembly rather than includingDafnyRuntime.csin the build process.
Legacy options:
-
-compile:<n>- [obsolete - usedafny buildordafny run] control whether compilation happens. The value of<n>can be one of the following. Note that if the program is compiled, it will be compiled to the target language determined by the-compileTargetoption, which is C# by default.-
0- do not compile the program -
1(default) - upon successful verification, compile the program to the target language. -
2- always compile, regardless of verification success. -
3- if verification is successful, compile the program (like option1), and then if there is aMainmethod, attempt to run the program. -
4- always compile (like option2), and then if there is aMainmethod, attempt to run the program.
-
-
-spillTargetCode:<n>- [obsolete - usedafny translate) control whether to write out compiled code in the target language (instead of just holding it in internal temporary memory). The value of<n>can be one of the following.-
0(default) - don't make any extra effort to write the textual target program (but still compile it, if-compileindicates to do so). -
1- write it out to the target language, if it is being compiled. -
2- write the compiled program if it passes verification, regardless of the-compilesetting. -
3- write the compiled program regardless of verification success and the-compilesetting.
-
Note that some compiler targets may (always or in some situations) write
out the textual target program as part of compilation, in which case
-spillTargetCode:0 behaves the same way as -spillTargetCode:1.
-
-Main:<name>- specify the (fully-qualified) name of the method to use as the executable entry point. The default is the method with the{:main}attribute, or else the method namedMain. -
-compileVerbose:<n>- control whether to write out compilation progress information. The value of<n>can be one of the following.-
0- do not print any information (silent mode) -
1(default) - print information such as the files being created by the compiler
-
-
-coverage:<file>- emit branch-coverage calls and outputs into<file>, including a legend that gives a description of each source-location identifier used in the branch-coverage calls. (Use-as<file>to print to the console.) -
-optimize- produce optimized C# code by passing the/optimizeflag to thecscexecutable. -
-optimizeResolution:<n>- control optimization of method target resolution. The value of<n>can be one of the following.-
0- resolve and translate all methods. -
1- translate methods only in the call graph of the current verification target. -
2(default) - as in1, but resolve only methods that are defined in the current verification target file, not in included files.
-
-
-testContracts:<mode>- test certain function and method contracts at runtime. This works by generating a wrapper for each function or method to be tested that includes a sequence ofexpectstatements for each requires clause, a call to the original, and sequence ofexpectstatements for eachensuresclause. This is particularly useful for code marked with the{:extern}attribute and implemented in the target language instead of Dafny. Having runtime checks of the contracts on such code makes it possible to gather evidence that the target-language code satisfies the assumptions made of it during Dafny verification through mechanisms ranging from manual tests through fuzzing to full verification. For the latter two use cases, having checks forrequiresclauses can be helpful, even if the Dafny calling code will never violate them.The
<mode>parameter can currently be one of the following.-
Externs- insert dynamic checks when calling any function or method marked with the{:extern}attribute, wherever the call occurs. -
TestedExterns- insert dynamic checks when calling any function or method marked with the{:extern}attribute directly from a function or method marked with the{:test}attribute.
-
Dafny builds on top of Boogie, a general-purpose intermediate language for verification. Options supported by Boogie on its own are also supported by Dafny. Some of the Boogie options most relevant to Dafny users include the following. We use the term "procedure" below to refer to a Dafny function, lemma, method, or predicate, following Boogie terminology.
-
--solver-path- specifies a custom SMT solver to use -
--solver-plugin- specifies a plugin to use as the SMT solver, instead of an external pdafny translaterocess -
--boogie- arguments to send to boogie
Legacy options:
-
-proc:<name>- verify only the procedure named<name>. The name can include*to indicate arbitrary sequences of characters. -
-trace- print extra information during verification, including timing, resource use, and outcome for each procedure incrementally, as verification finishes. -
-randomSeed:<n>- turn on randomization of the input that Boogie passes to the SMT solver and turn on randomization in the SMT solver itself.Certain Boogie inputs cause proof variability in the sense that changes to the input that preserve its meaning may cause the output to change. The
-randomSeedoption simulates meaning-preserving changes to the input without requiring the user to actually make those changes.The
-randomSeedoption is implemented by renaming variables and reordering declarations in the input, and by setting solver options that have similar effects. -
-randomSeedIterations:<n>- attempt to prove each VC<n>times with<n>random seeds. If-randomSeedhas been provided, each proof attempt will use a new random seed derived from this original seed. If not, it will implicitly use-randomSeed:0to ensure a difference between iterations. This option can be very useful for identifying input programs for which verification is highly variable. If the verification times or solver resource counts associated with each proof attempt vary widely for a given procedure, small changes to that procedure might be more likely to cause proofs to fail in the future. -
-vcsSplitOnEveryAssert- prove each (explicit or implicit) assertion in each procedure separately. See also the attribute{:isolate_assertions}for restricting this option on specific procedures. By default, Boogie attempts to prove that every assertion in a given procedure holds all at once, in a single query to an SMT solver. This usually performs well, but sometimes causes the solver to take longer. If a proof that you believe should succeed is timing out, using this option can sometimes help. -
-timeLimit:<n>- spend at most<n>seconds attempting to prove any single SMT query. This setting can also be set per method using the attribute{:timeLimit n}. -
-rlimit:<n>- set the maximum solver resource count to use while proving a single SMT query. This can be a more deterministic approach than setting a time limit. To choose an appropriate value, please refer to the documentation of the attribute{:rlimit}that can be applied per procedure. -
-print:<file>- print the translation of the Dafny file to a Boogie file.
If you have Boogie installed locally, you can run the printed Boogie file with the following script:
DOTNET=$(which dotnet)
BOOGIE_ROOT="path/to/boogie/Source"
BOOGIE="$BOOGIE_ROOT/BoogieDriver/bin/Debug/net8.0/BoogieDriver.dll"
if [[ ! -x "$DOTNET" ]]; then
echo "Error: Dafny requires .NET Core to run on non-Windows systems."
exit 1
fi
#Uncomment if you prefer to use the executable instead of the DLL
#BOOGIE=$(which boogie)
BOOGIE_OPTIONS="/infer:j"
PROVER_OPTIONS="\
/proverOpt:O:auto_config=false \
/proverOpt:O:type_check=true \
/proverOpt:O:smt.case_split=3 \
/proverOpt:O:smt.qi.eager_threshold=100 \
/proverOpt:O:smt.delay_units=true \
/proverOpt:O:smt.arith.solver=2 \
"
"$DOTNET" "$BOOGIE" $BOOGIE_OPTIONS $PROVER_OPTIONS "$@"
#Uncomment if you want to use the executable instead of the DLL
#"$BOOGIE" $BOOGIE_OPTIONS $PROVER_OPTIONS "$@"Much of controlling the prover is accomplished by controlling verification condition generation (25.9.7) or Boogie (Section 13.9.9). The following options are also commonly used:
-
--verification-error-limit:<n>- limits the number of verification errors reported per procedure. Default is 5; 0 means as many as possible; a small positive number runs faster but a large positive number reports more errors per run -
--verification-time-limit:<n>(was-timeLimit:<n>) - limits the number of seconds spent trying to verify each assertion batch.
Dafny is capable of generating unit (runtime) tests. It does so by asking the prover to solve for values of inputs to a method that cause the program to execute specific blocks or paths. A detailed description of how to do this is given in a separate document.
Footnotes
-
Files may be included more than once or both included and listed on the command line. Duplicate inclusions are detected and each file processed only once. For the purpose of detecting duplicates, file names are considered equal if they have the same absolute path, compared as case-sensitive strings (regardless of whether the underlying file-system is case sensitive). Using symbolic links may make the same file have a different absolute path; this will generally cause duplicate declaration errors. ↩
-
Unlike some languages, Dafny does not allow separation of declaration and implementation of methods, functions and types in separate files, nor, for that matter, separation of specification and declaration. Implementations can be omitted simply by leaving them out of the declaration (or a lemma, for example). However, a combination of
traitsandclassescan achieve a separation of interface and specification from implementation. ↩ -
The formula sent to the underlying SMT solver is the negation of the formula that the verifier wants to prove - also called a VC or verification condition. Hence, if the SMT solver returns "unsat", it means that the SMT formula is always false, meaning the verifier's formula is always true. On the other side, if the SMT solver returns "sat", it means that the SMT formula can be made true with a special variable assignment, which means that the verifier's formula is false under that same variable assignment, meaning it's a counter-example for the verifier. In practice and because of quantifiers, the SMT solver will usually return "unknown" instead of "sat", but will still provide a variable assignment that it couldn't prove that it does not make the formula true.
dafnyreports it as a "counter-example" but it might not be a real counter-example, only provide hints about whatdafnyknows. ↩ ↩2 ↩3 -
assume falsetells thedafnyverifier "Assume everything is true from this point of the program". The reason is that, 'false' proves anything. For example,false ==> Ais always true because it is equivalent to!false || A, which reduces totrue || A, which reduces totrue. ↩ -
assert P;. ↩ -
By default, the expression of an assertion or a precondition is added to the knowledge base of the
dafnyverifier for further assertions or postconditions. However, this is not always desirable, because if the verifier has too much knowledge, it might get lost trying to prove something in the wrong direction. ↩ ↩2 ↩3 ↩4 -
dafnyactually breaks things down further. For example, a preconditionrequires A && Bor an assert statementassert A && B;turns into two assertions, more or less likerequires A requires Bandassert A; assert B;. ↩ ↩2 -
All the complexities of the execution paths (if-then-else, loops, goto, break....) are, down the road and for verification purposes, cleverly encoded with variables recording the paths and guarding assumptions made on each path. In practice, a second clever encoding of variables enables grouping many assertions together, and recovers which assertion is failing based on the value of variables that the SMT solver returns. ↩
-
This post gives an overview of how assertions are turned into assumptions for verification purposes. ↩
-
Caveat about assertion and assumption: One big difference between an "assertion transformed in an assumption" and the original "assertion" is that the original "assertion" can unroll functions twice, whereas the "assumed assertion" can unroll them only once. Hence,
dafnycan still continue to analyze assertions after a failing assertion without automatically proving "false" (which would make all further assertions vacuous). ↩ -
To create a smaller batch,
dafnyduplicates the assertion batch, and arbitrarily transforms the clones of an assertion into assumptions except in exactly one batch, so that each assertion is verified only in one batch. This results in "easier" formulas for the verifier because it has less to prove, but it takes more overhead because every verification instance have a common set of axioms and there is no knowledge sharing between instances because they run independently. ↩