Upcoming

See docs/dev/news/.

4.1.0

New features

Added support for .toml based Dafny project files. For now the project file only allows specifying which Dafny files to include and exclude, and what options to use. The CLI commands that take Dafny files as input, such as build, run, translate, will now also accept Dafny project files. When using an IDE based on dafny server, such as the Dafny VSCode extension, the IDE will look for a Dafny project file by traversing up the file tree from the currently opened file, until it finds it dfyconfig.toml. The project file will override options specified in the IDE. (#2907)
Recognize the {:only} attribute on assert statements to temporarily transform other assertions into assumptions (#3095)
- Exposes the --output and --spill-translation options for the dafny test command (#3612)
The dafny audit command now reports instances of the {:concurrent} attribute, intended to flag code that is intended, but can't be proven, to be safe for use in a concurrent setting. (#3660)
Added option --no-verify for language server (#3732)
- Added .GetDocstring(DafnyOptions) to every AST node
- Plugin support for custom Docstring formatter,
- Activatable plugin to support a subset of Javadoc through --javadoclike-docstring-plugin
- Support for displaying docstring in VSCode (#3756)
Documentation of the syntax for docstrings added to the reference manual (#3773)
Labelled assertions and requires in functions (#3804)
API support for obtaining the Dafny expression that is being checked by each assertion (#3888)
Added a "Dafny Library" backend, which produces self-contained, pre-verified .doo files ideal for distributing shared libraries. .doo files are produced with commands of the form dafny build -t:lib .... (#3913)
Semantic interpretation of dots in names for {:extern} modules when compiling to Python (#3919)
Code actions in editor to explicit failing assertions. In VSCode, place the cursor on a failing assertion that support being made explicit and either
- Position the caret on a failing assertion, press CTRL+; and then ENTER
- Hover over the failing division by zero, click "quick fix", press ENTER Both scenarios will explicit the failing assertion. If you don't see a quick fix, it means that the assertion cannot be automatically made explicit for now.
Here is a initial list of assertions that can now be made explicit:
- Division by zero
- "out of bound" on sequences index, sequence slices, or array index
- "Not in domain" on maps
- "Could not prove unicity" of var x :| ... statement
- "Could not prove existence" of var x :| ... statement (#3940)

Bug fixes

- dafny test accepts a --methods-to-test option whose value is a regular expression selecting which tests to include in the test run (#3221)
- The deprecated attributes :dllimport, :handle, and :heapQuantifier are no longer recognized. (#3398)
While using dafny translate --target=java, the --include-sources option works as intended, while before it had no affect. (#3611)
Tested support for paths with spaces in them (#3683)
Crash related to the override check for generic functions (#3692)
Opaque functions guaranteed to be opaque until revealed (#3719)
Support for Corretto tests (#3731)
Right shift on native byte has the same consistent semantics even in Java (#3734)
- Main and {:test} methods may now be in the same program (#3744)
The formatter now produces the same output whether invoked on the command-line or from VSCode (#3790)
The --solver-log option is now hidden from help unless --help-internal is used. (#3798)
Highlight "inconclusive" as errors in the gutter icons (#3821)
Docstring for functions with ensures (#3840)
Prevent a compiler crash that could occur when a datatype constructor was defined that has multiple parameters with the same name. (#3860)
Improved rules for nameonly parameters and parameter default-value expressions (#3864)
Fixes several compilation issues, mostly related to subset types defined by one of its type parameter (#3893)
Explicitly define inequality of multisets in Python for better backwards compatibility (#3904)
Format for comprehension expressions (#3912)
Formatting for parameter default values (#3944)
Formatting issue in forall statement range (#3960)
Select alternative default calc operator only if it doesn't clash with given step operators (#3963)

4.0.0

Breaking changes

Remove deprecated countVerificationErrors option (#3165)
The default version of Z3 Dafny uses for verification is now 4.12.1. (#3400)
The default values of several options has changed in Dafny 4.0. See --help for details.
- --function-syntax changed from 3 to 4
- --quantifier-syntax changed from 3 to 4
- --unicode-char changed from false to true (#3623)
The default value of the /allocated option is now 4, and the option itself is deprecated. (#3637)
Compilation to Go no longer attempts to use the Dafny string type and the Go string type interchangably when calling external methods (which was buggy and unsound). (#3647)

3.13.1

New features

Expose non-relaxed definite assignment (/definiteAssignment:4) in legacy CLI (#3641)

Bug fixes

Fix translation of Dafny FunctionHandles to Boogie (#2266)
To ensure that a class correctly implements a trait, we perform an override check. This check was previously faulty across modules, but works unconditionally now. (#3479)
Fixes to definite assignment and determinism options:
- --enforce-determinism now forbids constructor-less classes
- With non-relaxed definite assignment, allow auto-init fields to be uninitialized (#3641)

3.12.0

New features

Dafny code formatter with IDE support (#2399)
- Makes it possible to "format" one or many Dafny files on the command-line, which for now means only changing the indentation of lines.
- Instructions and more details are available in the Dafny Reference Manual
Implements error detail information and quick fixes:
- An error catalog with error message explanations is at https://dafny.org/latest/HowToFAQ/Errors
- In VSCode, when hovering over an error, the hover information shows additional explanation and an error id, which is also a link to the error explanation page
- Where a Quick Fix is available, the Quick Fix link is active (#3299)
- opaque is now a modifier, though still allowed, but deprecated as an identifier; it replaces the {:opaque} attribute (#3462)
- The value of the --library option is allowed to be a comma-separated list of files or folders (#3540)

Bug fixes

Exclude verifier's type information for “new object” allocations (#3450)
The Dafny scanner no longer treats lines beginning with # (even those in strings) as pragmas. (#3452)
- The attribute :heapQuantifier is deprecated and will be removed in the future. (#3456)
Fixed race conditions in the language server that made gutter icons behave abnormally (#3502)
No more crash when hovering assertions that reference code written in other smaller files (#3585)

3.11.0

New features

Go to definition now works reliably across all Dafny language constructs and across files. (#2734)
Improve performance of Go code by using native byte/char arrays (#2818)
Introduce the experimental measure-complexity command, whose output can be fed to the Dafny report generator. In a future update, we expect to merge the functionality of the report generator into this command. (#3061)
Integrate the Dafny auditor plugin as a built-in dafny audit command. (#3175)
Add the --solver-path option to allow customizing the SMT solver used when using the new Dafny CLI user interface. (#3184)
Add the experimental --test-assumptions option to all execution commands: run, build, translate and test. When turned on, inserts runtime tests at locations where (implicit) assumptions occur, such as when calling or being called by external code and when using assume statements. Functionality is still being expanded. Currently only checks contracts on every call to a function or method marked with the {:extern} attribute. (#3185)
For the command translate, renamed the option --target into language and turned it into a mandatory argument. (#3239)
Havoc assignments now count as assignments for definite-assignment checks. (#3311)
Unless --enforce-determinism is used, no errors are given for arrays that are allocated without being initialized. (#3311)
Enable passing a percentage value to the --cores option, to use a percentage of the total number of logical cores on the machine for verification. (#3357)
dafny build for Java now creates a library or executable jar file.
- If there is a Main method, the jar is an executable jar. So a simple A.dfy can be built as dafny build -t:java A.dfy and then run as java -jar A.jar
- If there is no Main entry point, all the generated class files are assembled into a library jar file that can be used on a classpath as a java library.
- In both cases, the DafnyRuntime library is included in the generated jar.
- In old and new CLIs, the default location and name of the jar file is the name of the first dfy file, with the extension changed
- In old and new CLIs, the path and name of the output jar file can be given by the --output option, with .jar added if necessary
- As before, the compilation artifacts (.java and .class files) are placed in a directory whose name is the same as the jar file but without the .jar extension and with '-java' appended
- With the new CLI, the generated .java artifacts are deleted unless --spill-translation=true and the .class files are deleted in any case; both kinds of files are retained with the legacy CLI for backwards compatibility.
- If any other jar files are needed to compile the dafny/java program, they must be on the CLASSPATH; the same CLASSPATH used to compile the program is needed to run the program
Having a library or executable jar simplifies the user's task in figuring out how to use the built artifacts. (#3355)

Bug fixes

Nonexistent files passed on the CLI now result in a graceful exit (#2719)
Check loop invariants on entry, even when such are the only proof obligations in a method. (#3244)
The :options attribute now accepts new style options --function-syntax and --quantifier-syntax (#3252)
Improved error messages for dafny translate (#3274)
The :test attribute is now compatible with dafny run and dafny build (#3275)
Settings --cores=0 will cause Dafny to use half of the available cores. (#3276)
Removed an infeasible assertion in the Dafny Runtime for Java (#3280)
Language server displays more relevant information on hovering assertions (#3281)
Any (==) inferred for a type parameter of an iterator is now also inferred for the corresponding non-null iterator type. (#3284)
The otherwise ambiguous program fragment export least predicate is parsed such that least (or greatest) is the export identifier (#3291)
The parser no longer generates bad tokens when invoked through /library (#3301)
Match expressions no longer incorrectly convert between newtypes and their basetype (#3333)
Warn that 'new' cannot be used in expressions, instead of throwing a parse error (#3366)
The attributes :dllimport and :handle are now deprecated. They were undocumented, untested, and not maintained. (#3399)
Fixed an axiom related to sequence comprehension extraction (#3411)

3.10.0

New features

Emit warnings about possibly missing parentheses, based on operator precedence and unusual identation (#2783)
The DafnyRuntime NuGet package is now compatible with the .NET Standard 2.0 and .NET Framework 4.5.2 frameworks. (#2795)
Counterexamples involving sequences present elements in ascending order by index. (#2975)
The definition of the char type will change in Dafny version 4, to represent any Unicode scalar value instead of any UTF-16 code unit. The new command-line option --unicode-char allows early adoption of this mode. See section 7.5 of the Reference Manual for more details. (#3016)
dafny run now consistently requests UTF-8 output from compiled code. Use chcp 65501 if you see garbled output on Windows. (#3049)
feat: support for traits as type arguments by fully allowing variance on datatypes in Java (#3072)

Bug fixes

Function by method with the same name as a method won't crash resolver (#2019)
Better reporting if 'this' used in a subset type - and no crash (#2068)
Support for aliases in module resolution without crashing on imports (#2108)
Added missing check to prevent crash during resolution (#2111)
No more resolver crash on pattern match with incompatible types (#2139)
Refinements get errors at the correct place in LSP (#2402)
Resolution errors in the left-hand sign of an assign-such-that statement do not crash Dafny anymore (#2496)
old() cannot be inferred as a trigger alone (#2593)
Labels are no longer compiled in the case of variable declarations (#2608)
No more mention of reveal lemmas when implementing opaque functions in traits (#2612)
Verification of abstract modules not duplicated when imported (#2703)
Dafny now compiles functions that mix tail- and non-tail-recursive calls without crashing (#2726)
substitution of binding guards does not crash if splits present (#2748)
No more crash when constraining type synonyms (#2829)
Returning a tuple when it should be two variables does not crash Dafny anymore (#2878)
Default generic values no longer cause compilation error (#2885)
Now publishing Dafny Binary for MacOS Arm64 architecture (#2889)
Added a missing case in the Translator (pattern matching for variable declarations) (#2920)
The Python and Go backends now encode non-ASCII characters in string literals correctly (#2926)
Added a missing case of TypeSynonymDecl in the resolver that caused a crash (#2927)
Fix malformed Boogie generated for extreme predicates (#2984)
Counter-examples with non-integer sequence indices do not crash Dafny anymore. (#3048)
Use correct type for map update expression (#3059)
Language server no longer crashing in special case (#3062)
Resolved an instance in which the Dafny language server could enter a broken state. (#3065)
Do not refer to an implicit assignment in error messages on return statements (#3125)
Multiple exact same failing assertions do not crash the Boogie counter-example engine anymore (#3136)
Duplicate declarations caused by resolver do not crash the language server anymore (#3155)

3.9.1

New features

The language server now supports all versions of z3 ≥ 4.8.5. Dafny is still distributed with z3 4.8.5 and uses that version by default. (#2820)

Bug fixes

Correct error highlighting on function called with default arguments (#2826)
Crash in the LSP in some code that does not parse (#2833)
A function used as a value in a non-ghost context must not have ghost parameters, and arrow types cannot have ghost parameters. (#2847)
Compiled lambdas now close only on non-ghost variables (#2854)
Previously, for a file printing the number of arguments, dafny printing.dfy -compileTarget:js --args 1 2 3 would print 4: one for the executable, one for each argument. But dafny -compile:2 -compileTarget:js printing.dfy; node ./printing.js would print 5: One for node, one for ./printing.js, and one for each argument. This fix ensures that node ./printing.js is considered as a single argument, and the first argument, to be consistent with every other language. (#2876)
Handle sequence-to-string equality correctly in the JavaScript runtime (#2877)
don't crash on type synonyms and subset types of array types in LHSs of simultaneous assignments (#2884)
Removed an bogus optimization on the Language Server (#2890)
The Dafny-to-Java compiler will now fully-qualify type casts in pattern destructors, avoiding "reference to TYPE is ambiguous" errors from javac. (#2904)
Variable declarations and formals in match cases do not trigger errors anymore. (#2910)

3.9.0

feat: Introduce a new Dafny CLI UI that complies with the POSIX standard and uses verbs to distinguish between use-cases. Run the Dafny CLI without arguments to view help for this new UI. (#2823)
feat: Support for testing certain contracts at runtime with a new /testContracts flag (#2712)
feat: Support for parsing Basic Multilingual Plane characters from UTF-8 in code and comments (#2717)
feat: Command-line arguments are now available from Main in Dafny programs, using Main(args: seq<string>) (#2594)
feat: Generate warning when 'old' has no effect (#2610)
fix: Missing related position in failing precondition (#2658)
fix: No more IDE crashing on the elephant operator (#2668)
fix: Use the right comparison operators for bitvectors in Javascript (#2716)
fix: Retain non-method-body block statements when cloning abstract signatures (#2731)
fix: Correctly substitute variables introduced by a binding guard (#2745)
fix: The CLI no longer attempts to load each DLL file passed to it. (#2568)
fix: Improved hints and error messages regarding variance/cardinality preservation (#2774)
feat: New behavior for import opened M where M contains a top-level declaration M, see PR for a full description (#2355)
fix: The DafnyServer package is now published to NuGet as well, which fixes the previously-broken version of the DafnyLanguageServer package. (#2787)
fix: Support for spaces in the path to Z3 (#2812)
deprecate: Statement-level refinement syntax (e.g. assert ...) is deprecated (#2756)
deprecate: The form of the modify statement with a block statement is deprecated
docs: The user documentation at https://dafny.org has a new landing page

3.8.1

feat: Support for the {:opaque} attibute on const (#2545)
feat: Support for plugin-based code actions on the IDE (#2021)
fix: Fixed a crash when parsing newtype in the parser (#2649)
fix: Added missing error reporting position on string prefix check (#2652)
fix: Prevent LSP server from exiting when a crash occurs (#2664)
fix: Fix bug where LSP server would not show diagnostics that referred to included files (#2664)
fix: Check all compiled expressions to be compilable (#2641)
fix: Better messages on hovering failing postconditions in IDE (#2654)
fix: Better error reporting on counter-examples if an option is not provided (#2650)
feat: Introduced ghost constructors in datatypes. One use of these is when working with uninitialized storage, see dafny-lang/rfcs#11. (#2666)

3.8.0

fix: Use the right bitvector comparison in decrease checks (#2512)
fix: Don't use native division and modulo operators for non-native int-based newtypes in Java and C#. (#2416)
feat: Dafny now supports disjunctive (“or”) patterns in match statements and expressions. Cases are separated by | characters. Disjunctive patterns may not appear within other patterns and may not bind variables. (#2448)
feat: The Dafny Language Server used by the VSCode IDE extension is now available as a NuGet package called DafnyLanguageServer (#2600)
fix: Counterexamples - fix an integer parsing bug and correctly extract datatype and field names (#2461)
feat: New option -diagnosticsFormat:json to print Dafny error messages as JSON objects (one per line). (#2363)
fix: No more exceptions when hovering over variables without type, and types of local variabled kept under match statements (#2437)
fix: Check extreme predicates and constants in all types, not just classes (#2515)
fix: Correctly substitute type variables in override checks (#2522)
feat: predicate P(x: int): (y: bool) ... is now valid syntax (#2454)
fix: Improve the performance of proofs involving bit vector shifts (#2520)
fix: Perform well-definedness checks for ensures clauses of forall statements (#2606)
fix: Resolution and verification of StmtExpr now pay attention to if the StmtExpr is inside an 'old' (#2607)

3.7.3

feat: Less code navigation when verifying code: In the IDE, failing postconditions and preconditions error messages now immediately display the sub-conditions that Dafny could not prove. Both on hover and in the Problems window. (#2434)
feat: Whitespaces and comments are kept in relevant parts of the AST (#1801)
fix: NuGet packages no longer depend on specific patch releases of the .NET frameworks.

3.7.2

fix: Hovering over variables and methods inside cases of nested match statements works again. (#2334)
fix: Fix bug in translation of two-state predicates with heap labels. (#2300)
fix: Check that arguments of 'unchanged' satisfy enclosing reads clause. (#2302)
feat: Whitespaces and comments are kept in relevant parts of the AST (#1801)
fix: Underconstrained closures don't crash Dafny anymore. (#2382)
fix: Caching in the language server does not prevent gutter icons from being updated correctly. (#2312)
fix: Last edited file verified first & corrected display of verification status. (#2352)
fix: Correctly infer type of numeric arguments, where the type is a subset type of a newtype. (#2314)
fix: Fix concurrency bug that sometimes led to an exception during the production of verification logs. (#2398)

3.7.1

fix: The Dafny runtime library for C# is now compatible with .NET Standard 2.1, as it was before 3.7.0. Its version has been updated to 1.2.0 to reflect this. (#2277)
fix: Methods produced by the test generation code can now be compiled directly to C# XUnit tests (#2269)

3.7.0

feat: The Dafny CLI, Dafny as a library, and the C# runtime are now available on NuGet. You can install the CLI with dotnet tool install --global Dafny. The library is available as DafnyPipeline and the runtime is available as DafnyRuntime. (#2051)
feat: New syntax for quantified variables, allowing per-variable domains (x <- C) and ranges (x | P(x), y | Q(x, y)). See the quantifier domain section of the Reference Manual. (#2195)
feat: The IDE will show verification errors for a method immediately after that method has been verified, instead of after all methods are verified. (#2142)
feat: Added "Resolving..." message for IDE extensions (#2234)
feat: Live verification diagnostics for the language server (#1942)
fix: Correctly specify the type of the receiver parameter when translating tail-recursive member functions to C# (#2205)
fix: Added support for type parameters in automatically generated tests (#2227)
fix: No more display of previous obsolete verification diagnostics if newer are available (#2142)
fix: Prevent the language server from crashing and not responding on resolution or ghost diagnostics errors (#2080)
fix: Various improvements to language server robustness (#2254)

3.6.0

feat: The synthesize attribute on methods with no body allows synthesizing objects based on method postconditions at compile time (currently only available for C#). See Section 22.2.20 of the Reference Manual. (#1809)
feat: The /verificationLogger:text option now prints all verification results in a human-readable form, including a description of each assertion in the program.
feat: The /randomSeedIterations:<n> option (from Boogie) now tries to prove each verification condition n times with a different random seed each time, to help efficiently and conveniently measure the stability of verification. (boogie-org/boogie#567)
feat: The new /runAllTests can be used to execute all methods with the {:test} attribute, without depending on a testing framework in the target language.
feat: Recognize !in operator when looking for compilable comprehensions (#1939)
feat: The Dafny language server now returns expressions ranges instead of token ranges to better report errors (#1985)
fix: Miscompilation due to incorrect parenthesization in C# output for casts. (#1908)
fix: Populate TestResult.ResourceCount in /verificationLogger:csv output correctly when verification condition splitting occurs (e.g. when using /vcsSplitOnEveryAssert).
fix: DafnyOptions.Compiler was null, preventing instantiation of ModuleExportDecl (#1933)
fix: /showSnippets crashes Dafny's legacy server (#1970)
fix: Don't check for name collisions in modules that are not compiled (#1998)
fix: Allow datatype update expressions for constructors with nameonly parameters (#1949)
fix: Fix malformed Java code generated for comprehensions that use maps (#1939)
fix: Comprehensions with nested subset types fully supported, subtype is correctly checked (#1997)
fix: Fix induction hypothesis generated for lemmas with a receiver parameter (#2002)
fix: Make verifier understand (!new) (#1935)
feat: Some command-line options can now be applied to individual modules, using the {:options} attribute. (#2073)
fix: Missing subset type check in datatype updates (#2059)
fix: Fix initialization of non-auto-init in-parameters in C#/JavaScript/Go compilers (#1935)
fix: Resolution of static functions-by-method (#2023)
fix: Export sets did not work with inner modules (#2025)
fix: Prevent refinements from changing datatype and newtype definitions (#2038)
feat: The new older modifier on arguments to predicates indicates that a predicate ensures the allocatedness of some of its arguments. This allows more functions to show that their quantifiers do not depend on the allocation state. For more information, see the reference manual section on older. (#1936)
fix: Fix (!new) checks (#1419)
fix: multiset keyword no longer crashes the parser (#2079)

3.5.0

feat: continue statements. Like Dafny's break statements, these come in two forms: one that uses a label to name the continue target and one that specifies the continue target by nesting level. See section 19.2 of the Reference Manual. (#1839)
feat: The keyword syntax for functions will change in Dafny version 4. The new command-line option /functionSyntax (see /help) allows early adoption of the new syntax. (#1832)
feat: Attribute {:print} declares that a method may have print effects. Print effects are enforced only with /trackPrintEffects:1.
fix: No warning "File contains no code" if a file only contains a submodule (#1840)
fix: Stuck in verifying in VSCode - support for verification cancellation (#1771)
fix: export-reveals of function-by-method now allows the function body to be ghost (#1855)
fix: Regain C# 7.3 compatibility of the compiled code. (#1877)
fix: The error "assertion violation" is replaced by the better wording "assertion might not hold". This indicates better that the verifier is unable to prove the assertion. (#1862)
fix: Plug two memory leaks in Dafny's verification server (#1858, #1863)
fix: Generate missing termination measures for subset types on sequences (#1875)
fix: Resolve expressions in attributes in all specifications of functions and iterators. (#1900)

3.4.2

fix: No output when compiling to JavaScript on Windows (#1824)
fix: CanCall assumptions for loop invariants (#1813)
fix: Behavior of the C# runtime in a concurrent setting (#1780)

3.4.1

feat: Plugin support in the resolution pipeline (#1739)
fix: NullPointerException in the AST (#1805)
fix: Change datatype deconstruction in match statements for C# (#1815)

3.4

For certain classes of changes to a Dafny program, prevent unexpected changes in verification behavior.
Add command line options to assist in debugging verification performance.
Critical fixes to the IDE and greatly improved responsiveness of non-verification IDE features.
The C# back-end supports traits as type parameters on datatypes.

Verification

feat: Prevent changes in the verification behavior of a proof, when any of these types of changes are made to Dafny user code:
- Changes to declarations not referenced by the method being verified
- Changes to the name of any declaration
- Changes to the order of top-level declarations
feat: Assist in debugging the verification performance of a proof by adding the /vcsSplitOnEveryAssert CLI option and {:vcs_split_on_every_assert} attribute (see boogie-org/boogie#465), and report the outcome and duration of splits when they occur in /verificationLogger:trx content.
feat: Add a /verificationLogger:csv CLI option that emits the same status and timing information as /verificationLogger:trx, but in an easier-to-parse format, along with Z3 resource counts for more repeatable tracking of verification difficulty.
fix: Resolve unsoundness issue (#1619).
fix: Don't silently succeed if the solver crashes (boogie-org/boogie#488).

IDE

feat: Verification status reporting shows which proof is being verified, which can help debug slow to verify proofs.
feat: Publish parsing and resolution diagnostics before verification has completed. Verification diagnostics from previous runs are migrated.
feat: Enable 'go to definition', 'hover' and 'signature help' features before verification has completed.
feat: Improve the hover feature to work for a wider scope of Dafny constructs, including function and method parameters, forall, exists and let expressions, and set and map comprehensions.
feat: Add an experimental verification caching feature, which enables automatically determining which proofs need to verify again after making changes.
feat: Display related resolution errors using nested diagnostics instead of independent diagnostics.
fix: Clean up process resources if IDE closed or restarted.
fix: Do not let the Dafny compilation status bar get in a stuck state.

UX

feat: Improve error reporting when providing incorrectly typed arguments in a function call.
feat: Improve error reporting when using type tests.

C#

feat: Support variant type parameters on datatype definitions, which enables using traits as type arguments (#1499).
feat: Support for downcasting both custom datatypes and functions (#1645, #1755).
fix: Resolve various instances where Dafny would produce invalid C# code (#1607, #1761, and #1762).

Various improvements

fix: DafnyLanguageServer.dll and Dafny.dll depended on two different versions of Newtonsoft.Json, which could cause crashes in development environments.
fix: (error reporting) Types with the same name but from different modules are now disambiguated in error messages.
fix: (error reporting) Messages about arguments / parameters type mismatch are clearer and include the parameter name if available.
fix: (robustness) Exceptions during parsing, if any, won't crash the language server anymore.
fix: The elephant operator (:-) has a clearer error message and no longer reject generic methods on its right-hand side.

Breaking changes

The verifier in Dafny 3.4 is now more efficient for many programs, and making changes to Dafny programs is less likely to cause verification to take longer or timeout. However, it is still possible for some correct programs to take longer to verify than on Dafny 3.3, or for verification to fail. For users with such programs who are not yet ready to modify them to pass the 3.4 verifier, we offer the command line option /mimicVerificationOf:3.3 to keep the Dafny 3.4 verification behavior consistent with 3.3.

In Dafny 3.3, comprehensions quantified over subset types did not validate the constraint of the subset type, which could result in crashes at run-time. In 3.4, subset types are disabled in set comprehensions in compiled contexts, unless the subset constraint is itself compilable.

Before, the following code would pass Dafny and be compiled without error, but would crash at run-time:

type RefinedData = x: Data | ghostFunction(x)
method Main() {
  var s: set<Data> = ...
  var t = set x: RefinedData | x in s;
  forall x in t {
    if !ghostFunction(x) {
      var crash := 1/0;
    }
  }
}

In Dafny 3.4, the same code triggers a resolution error of the form:

Error: RefinedData is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. The next error will explain why the constraint is not compilable.
Error: ghost constants are allowed only in specification contexts

Changes in type inference may cause some programs to need manual type annotations. For example, in the nested pattern in the following program

datatype X<+T> = X(x: T)
datatype Y<T> = Y(y: T)

function method M(): (r: X<Y<nat>>) {
    var d: X<Y<int>> := X(Y(3));
    match d
    case X(Y(i)) => X(Y(i))
}

the type of the Y constructor needs the type to be given explicitly X(Y<nat>.Y(i). As a variation of that program

datatype X<+T> = X(x: T)
datatype Y<T> = Y(y: T)

trait Tr {}
class Cl extends Tr {
    constructor () {}
}

method M() returns (r: X<Y<Cl>>) {
    var cl := new Cl();
    var d: X<Y<Tr>> := X(Y(cl));
    match d
    case X(Y(tr)) => r := X(Y(tr));
}

the program can be specified with an explicit cast X(Y(tr as Cl)).

Files

RELEASE_NOTES.md

Latest commit

History

RELEASE_NOTES.md

File metadata and controls

Upcoming

4.1.0

New features

Bug fixes

4.0.0

Breaking changes

3.13.1

New features

Bug fixes

3.12.0

New features

Bug fixes

3.11.0

New features

Bug fixes

3.10.0

New features

Bug fixes

3.9.1

New features

Bug fixes

3.9.0

3.8.1

3.8.0

3.7.3

3.7.2

3.7.1

3.7.0

3.6.0

3.5.0

3.4.2

3.4.1

3.4

Verification

IDE

UX

C#

Various improvements

Breaking changes