Skip to content

Quick migration guide from Dafny 3.X to Dafny 4.0

Jump to bottom
Clément Pit-Claudel edited this page Mar 22, 2023 · 25 revisions

Migration to Dafny 4.0

TL;DR

  • Dafny now has a verb-oriented command-line (dafny run ..., dafny verify ... etc.), which you are encouraged to use. Some defaults are changed when using the new CLI.
  • Change plain function to ghost function and function method to function. Same for predicate.
    method and function ... by method stays the same.
  • Surround set comprehensions without a :: and followed by a comma by a set of (); new parsing rules capture that comma by the set comprehension
  • The default for --unicode-char is now true instead of false. Use an explicit option to select one or the other, if needed.
  • The PropagateFailure and Extract members of a failure-compatible type are expected to be functions, not methods. Having them be methods is deprecated and will become illegal with Dafny 4.
  • opaque is now a keyword and may not be used as an identifier. It replaces the attribute {:opaque}, which is now deprecated.
  • These previously deprecated attributes are removed: :heapQuantifier, :dllimport, :handle.
  • This previously deprecated option is removed: /countVerificationErrors
  • Dafny uses a new version of Z3 by default (4.12.1), though it is still compatible with older Z3 versions. Some proofs may need to be updated to successfully verify.
  • We have begun the task of developing a set of Dafny libraries (see notes below).
  • The IDE itself has new functionality. For example, we've started to add error explanations (both here and in the hover information of the IDE) and quick fixes, with more to come.

These changes are described briefly below. The Reference Manual gives more detail.

Command-line

Dafny now has a command-oriented command-line syntax, like many other tools (git, for example). Command-lines are written as dafny <verb> <files, folders, options> where the verbs execute a number of common operations:

  • dafny resolve - just parse and type-check the files (like the previous /compile:0 /noVerify)
  • dafny verify - parse, type-check, and verify the files (like /compile:0)
  • dafny translate <target language> - parse, type-check, verify (unless --no-verify is an option), and translate to target language source code (like `/compile:0 /spillTargetCode:3)
  • dafny build - all of translate plus compiling the source code to an executable (e.g. an .exe or .dll or executable .jar) (like /compile:2)
  • dafny run - build and run a Dafny program (like compile:4)

These commands take different sets of options appropriate to their function. And the options are now in double-hyphen style.

In addition, the Dafny team is adding other kinds of operations. For example

  • dafny format to reformat source code in a standard style
  • dafny audit to report possible soundness problems in the target code
  • dafny test to run executable tests Plus other such tools are under discussion or development or experimentation.

Changes in option defaults

With the change to the new CLI and option style, there are some changes in defaults and renamings of options (e.g. /timeLimit to --verification-time-limit)

Definite assignment

The rules around definite assignment are now stricter, to aid in assuring soundness and determinism. There are three combinations to think about:

  • --enforce-determinism : enforces a strict rule of variables needing to be assigned a value before they are used and that all compiled constructs must be deterministic, so that the resulting programs produce the same results on each run
  • (default) : strict definite assignment, but not necessarily deterministic
  • --relax-definite-assignment : more relaxed rules abut definite assignment Note that 'definite assignment' means that there was an assignment to a variable, not that it is known what the assigned value is.

As an example of the change:

method m() returns (r: int) {
  var i: int;
  return i;
}

has no complaints with --relax-definite-assignment, but will provoke an error with the default.

However,

method m() returns (r: int) {
  var i: int := *;
  return i;
}

is OK with the default setting (i is given an arbitrary value), but will provoke an error if compiled with --enforce-determinism.

Verbosity

-compileVerbose is now --verbose and is by default off

Function keywords

After careful consideration and debate, the Dafny designers decided to simplify the cumbersome "function method" keyword that indicated a compiled function, and replace it with simply "function", despite the backwards incompatibility this causes. Now ghost functions and methods are declared the same way --- with a ghost modifier.

With Dafny 4.0, the keyword pair "function method" is no longer use, only the "ghost" keyword is used, like for methods and variables:

Dafny 3: Dafny 4: Changed?
Ghost declarations
predicate P() {} ghost predicate() {} Different
function F() {} ghost function() {} Different
twostate predicate P() {} twostate predicate P() {} Same
least predicate P() {} least predicate P() {} Same
greatest predicate P() {} greatest predicate P() {} Same
twostate function F() {} twostate function F() {} Same
static predicate P() {} // In types with members static ghost predicate P() {} Same
static function P() {} // In types with members static ghost function P() {} Same
ghost method M() {} ghost method M() {} Same
static ghost method M() {} static ghost method M() {} Same
Compiled declarations
function method F() {} function F() {} Different
predicate method F() {} predicateF() {} Different
static predicate method P() {} // In types with members static predicate P() {} Same
static function method P() {} // In types with members static function P() {} Same
method M() {} method M() {} Same
static method M() {} static method M() {} Same

Migration instructions

If you don't want to migrate now, and/or you want to ensure your code will compile even with an updated version of 4.0, you can compile with the option --function-syntax:3, or define it on a per-module basis, like this:

module {:options "--function-syntax:3"} MyModule {
  // Dafny 3-like code.
}

Now, if you are ready to make the change, it's quite easy

  1. Ensure there are no more {:options "--function-syntax:3"} in your code.
  2. Look for the regex (?<!(?:twostate|least|greatest)\s+)(function|predicate)(?!\s+method) in your code and replace it by ghost $1
  3. Look for the regex (function|predicate)\s+method and replace it by $1

You can also make the change in two steps, which helps assure that nothing is missed, using --function-syntax:migration3to4.

  1. Start with a program P that compiles without error with command-line option --function-syntax:3, and there are no more {:options "--function-syntax:3"} in your code.
  2. Change to using --function-syntax:migration3to4. The effect of this is to require ghost function instead of function (similarly for predicate), while leaving function method as legal. So now all function declarations will be parse errors and they can be readily spotted and changed to ghost function.
  3. Then change to --function-syntax:4. Now the function method declarations are errors and can be spotted and changed to function declarations.

Quantifier Syntax

We decided to support multiple per-variable ranges in comprehensions, separated by commas.

Before, the these two statements were equivalent

print set x | 0 <= x < 10, y
print (set x | 0 <= x < 10), y

With Dafny 4.0, these become equivalent to the following

print set x | 0 <= x < 10, y
print (set x | 0 <= x < 10, y)

To keep the old meaning, write

print (set x | 0 <= x < 10), y

Migration instructions

This change is likely to have minimal impact. If you don't want to migrate now, and/or you want to ensure your code will compile even with an updated version of 4.0, you can compile with the option --quantifier-syntax:3, or define it on a per-module basis, like this:

module {:options "--quantifier-syntax:3"} MyModule {
  // Dafny 3-like code.
}

You can even define multiple options like this:

module {:options "--function-syntax:3 --quantifier-syntax:3"} MyModule {
  // Dafny 3-like code.
}

If you are ready to migrate,

  • Ensure there is no more {:options "--quantifier-syntax:3"} in your code.
  • Only set comprehensions are sensitive to this change (because the :: is optional).
  • Look at all the set(?!<) to find all the set comprehensions, and verify that they are not followed by a comma that could be captured by the set comprehension.
  • If that the case, wrap your comprehensions with parentheses, or provide an explicit term using :: like set x <- xs :: x.

The built-in char type

The char type in Dafny previously always had the same meaning as in languages such as Java and C#: any 16-bit value. The string type, which is (and remains) always a synonym for seq<char>, was therefore implicitly always encoded in UTF-16. This allowed invalid data, however: the Unicode standard specifies that surrogate code points always have to be used in valid pairs, but Dafny provided no such guarantee, and so, for example, any function to encode a Dafny string in UTF-8 had to be partial in order to reject this invalid data.

The --unicode-char option was introduced to change the meaning of char to be any Unicode scalar value, the same as the Rust char or Go rune type. With this option enabled, a seq<char> is at least always a valid Unicode string for interchange. In Dafny 4.0, this option is enabled by default.

The option also has two other, more minor side-effects:

  1. String and character literals no longer support \uXXXX escape sequences for UTF-16 code points, and instead support \U{X..X} Unicode scalar value escape sequences of up to six characters. See http://dafny.org/dafny/DafnyRef/DafnyRef#sec-characters for details.
  2. The printed form of characters and strings becomes more consistent across all backends. This is not strongly specified in the Dafny language, but the details are described in this note.

Migration instructions

This change is unlikely to cause any verification changes in most codebases. If anything, a verification failure is likely to indicate hidden assumptions about how strings are being processed! As with the other options, you can choose to opt-out of the new behavior using the --unicode-char:false option.

If you have existing code that depends on a 16-bit wide definition of char, you can define your own custom type to use instead:

newtype char16 = c: int | 0 <= c < 0x1_0000

--unicode-char changes the runtime representation of the char type, and so if you have {:extern} definitions that use string or char in their signatures, it will cause compilation or runtime errors, depending on the target programming language. The details of what types are used in each backend are documented here.

Z3 version

For several years, Dafny has been distributed and tested with Z3 version 4.8.5. With Dafny 4.0, we have updated the default Z3 version to 4.12.1. Due to a large number of accumulated changes in Z3, some proofs that go through with 4.8.5 will not go through with 4.12.1. In general, these tend to be proofs that depend on large definitions or make heavy use of universally or existentially quantified predicates.

To evaluate your code with Z3 4.12.1 while still using Dafny 3.x:

  • Download a Z3 4.12.1 binary from here
  • Run Dafny with --solver-path /path/to/z3 or /proverOpt:PROVER_PATH=/path/to/z3

To continue using Z3 4.8.5 with Dafny 4.0:

  • Download a Z3 4.8.5 binary from here
  • Run Dafny with --solver-path /path/to/z3 or /proverOpt:PROVER_PATH=/path/to/z3

To update your proofs to work with Z3 4.12.1, the sections on making proofs go through and speeding up slow proofs in the reference manual may be helpful.

Dafny libraries

We need your input!

We have begun the task of developing a set of Dafny libraries -- basic functionality that is needed by many Dafny users. Documentation and a draft reorganization of the existing modules is in Dafny's github repository. In particular, the development team would like your input as to what functionality is most important. As important are the overall goals for these libraries:

  • be stable
  • contain useful functionality
  • uses of library code prove efficiently
  • compilations of the library code are available on all platforms (as much as possible) and run efficiently
  • as befits the term 'library', it is possible to automatically use just the portions of the code that are needed for a given program
  • is packaged conveniently for end-user use
Clone this wiki locally