Dafny Changelog

What's new in Dafny 4.6.0

Mar 28, 2024

New features:
Add a check to dafny run that notifies the user when a value that was parsed as a user program argument, and which occurs before a -- token, starts with --, since this indicates they probably mistyped a Dafny option name. (#5097)
Add an option --progress that can be used to track the progress of verification. (#5150)
Add the attribute {:isolate_assertions}, which does the same as {:vcs_split_on_every_assert}. Deprecated {:vcs_split_on_every_assert} (#5247)
Bug fixes:
(soundness issue) Twostate predicate now check if their not new arguments are allocated in the previous heap (#4844)
Add uniform checking of type characteristics in refinement modules (#5146)
Fixed links associated with the standard libraries. (#5176)
Fix: Disable the "erase datatype wrappers" optimization if the datatype implements any traits.
Feat: Allow the "erase datatype wrappers" optimization if the only fields in the datatype are ghost fields.
(#5234)
Fix the default string value emitted for JavaScript (#5239)

New in Dafny 4.5.0 (Mar 16, 2024)

New features:
Add the option --include-test-runner to dafny translate, to enable getting the same result as dafny test when doing manual compilation. (#3818)
Fix: verification in the IDE no longer fails for iterators
Fix: the IDE now provides feedback when verification fails to run, for example due to a bad solver path
Fix: let the IDE correctly use the solver-path option when it's specified in a project file
Feat: improve the order of verification diagnostics emitted by the Dafny CLI, so that they now always follow the line order of the program.(#4798)
Add an option --filter-position to the dafny verify command. The option filters what gets verified based on a source location. The location is specified as a file path suffix, optionally followed by a colon and a line number. For example, dafny verify dfyconfig.toml --filter-position=source1.dfy:5 will only verify things that range over line 5 in the file source1.dfy. In combination with ``--isolate-assertions, individual assertions can be verified by filtering on the line that contains them. When processing a single file, the filename can be skipped, for example: dafny verify MyFile.dfy --filter-position=:23`
Add an option --filter-symbol to the dafny verify command, that only verifies symbols whose fully qualified name contains the given argument. For example, dafny verify dfyconfig.toml --filter-symbol=MyModule will verify everything inside MyModule.
The option --boogie-filter has been removed in favor of --filter-symbol (#4816)
Add a json format to those supported by --log-format and /verificationLogger, for producing thorough, machine readable logs of verification results. (#4951)
Flip the behavior of --warn-deprecation and change the name to --allow-deprecation, so the default is now false, which is standard for boolean options.
When using --allow-deprecation, deprecated code is shown using tooltips in the IDE, and on the CLI when using --show-tooltips.
Replace the option --warn-as-error with the option --allow-warnings. The new option, when false, the default value, causes Dafny to stop generating executable output and return a failure exit code, when warnings occur in the program. Contrary to the previous --warn-as-error option, warnings are always reported as warnings.
During development, users must use dafny run --allow-warnings if they want to run their Dafny code when it contains warnings.
If users have builds that were passing with warnings, they have to add --allow-warnings to allow them to still pass.
If users upgrade to a new Dafny version, and are not using --allow-warnings, and do not want to migrate off of deprecated features, they will have to use --allow-deprecation.
When using the legacy CLI, the option /warningsAsErrors now has the behavior of --allow-warnings=false
A doo file that was created using --allow-warnings causes a warning if used by a consumer that does not use it. (#4971)
The new {:contradiction} attribute can be placed on an assert statement to indicate that it forms part of an intentional proof by contradiction and therefore shouldn't be warned about when --warn-contradictory-assumptions is turned on. (#5001)
Function and method parameters and return types, and datatype constructor arguments, can now have attributes. By default, there are no attributes that Dafny recognizes in these positions, but custom back-ends can use this feature to get extra information from the source files. (#5032)
Under the CLI option --general-newtypes, the base type of a newtype declaration can now be (int or real, as before, or) bool, char, or a bitvector type.
as and is expressions now support more types than before. In addition, run-time type tests are supported for is expressions, provided type parameters are injective (as was already required) and provided the constraints of any subset type or newtype is compilable. Note, although both as and is allow many more useful cases than before, using --general-newtypes will also forbid some unusual cases that were previously allowed. Any such case that is now forbidden can still be done by doing the as/is via int. (#5061)
Allow newtype declarations to be based on set/iset/multiset/seq. (#5133)
Bug fixes:
Fixed crash caused by cycle in type declaration (#4471)
Fix resolution of unary minus in new resolver (#4737)
The command line and the language server now use the same counterexample-related Z3 options. (#4792)
Dafny no longer crashes when required parameters occur after optional ones. (#4809)
Use defensive coding to prevent a crash in the IDE that could occur in the context of code actions. (#4818)
Fix null-pointer problem in new resolver (#4875)
Fixed a crash that could occur when a case body of a match that was inside a loop, had a continue or break statement. (#4894)
Compile run-time constraint checks for newtypes in comprehensions (#4919)
Fix null dereference in constant-folding invalid string-indexing expressions (#4921)
Check for correct usage of type characteristics in specifications and other places where they were missing.
This fix will cause build breaks for programs with missing type characteristics (like (!new) and (0)). Any such error message is accompanied with a hint about what type characterics need to be added where. (#4928)
Initialize additional fields in the AST (#4930)
Fix crash when a function/method with a specification is overridden in an abstract type. (#4954)
Fix crash for lookup of non-existing member in new resolver (#4955)
Fix: check that subset-type variable's type is determined (resolver refresh).
Fix crash in verifier when there was a previous error in determining subset-type/newtype base type.
Fix crash in verifier when a subset type has no explicit witness clause and has a non-reference trait as its base type. (#4956)
The {:rlimit N} attribute, which multiplied N by 1000 before sending it to Z3, is deprecated in favor of the {:resource_limit N} attribute, which can accept string arguments with exponential notation for brevity. The --resource-limit and /rlimit flags also now omit the multiplication, and the former allows exponential notation. (#4975)
Allow a datatype to depend on traits without being told "datatype has no instances" (#4997)
Don't consider := * to be a definite assignment for non-ghost variables of a (00) type (#5024)
Detect the same ghost usage in initializing assignments as in other expressions. The effect of this fix is to allow more iset/imap comprehensions to be compiled.
Also, report errors if the LHS of := in compiled map/imap comprehensions contains ghosts. (#5041)
Escape names of nested modules in C# and Java (#5049)
A parent trait that is a reference type can now be named via import opened.
Implicit conversions between a datatype and its parent traits no longer crashes the verifier.
(Dis)equality expressions of a (co)datatype and its parent traits no longer crashes the verifier. (#5058)
Fixed support for newtypes as sequence comprehension lengths in Java (#5065)
Don't emit an error message for a function-by-method with unused type parameters. (#5068)
The syntax of a predicate definition must always include parentheses. (#5069)
Termination override check for certain non-reference trait implementations (#5087)
Malformed Python code for some functions involving lambdas (#5093)
Let verifier understand opaque function overrides, supporting both when the overridden function is opaque and non-opaque. Revealing such a function for one overriding type has the effect of revealing it for all overriding types.
Also, forbid the case where a function is opaque in a parent trait and the function override is not opaque. (Previously, this had caused a crash.)

New in Dafny 4.3.0 (Sep 29, 2023)

New features:
Add support for the Find References LSP request
Returned references may be incomplete when not using project mode
(#2320)
Improve scalability of inlining for test generation and generate coverage information with respect to the original Dafny source (#4255)
Support generating of tests targeting path-coverage of the entire program and tests targeting call-graph-sensitive block coverage (referred to as Branch coverage) (#4326)
Add support for Rename LSP request
Support requires enabling project mode and defining a Dafny project file
(#4365)
Make verification in the IDE more responsive by starting verification after translating the required module to Boogie, instead of first translating all modules that could be verified. (#4378)
The Dafny IDE now has improved behavior when working with a Dafny file that's part of a Dafny project. A Dafny file is part of a project if a dfyconfig.toml can be found somewhere in the file's path hierarchy, such as in the same folder or in the parent folder. A dfyconfig.toml can specify which Dafny options to use for that project, and can specify which Dafny files are part of the project. By default, the project will include all .dfy files reachable from the folder in which the dfyconfig.toml resides. Project related features of the IDE are:
Whenever one file in the project is opened, diagnostics for all files in the Dafny project are shown. When including a file with errors that's part of the same project, the message "the included file contains errors" is no longer shown. Instead, the included file's errors are shown directly.
If any file in the project is changed, diagnostics for all files in the project are updated. Without a project, changing an included file will not update diagnostics for the including file until the including file is also changed.
The find references feature (also added in this release), works better in files that are part of a project, since only then can it find references that are inside files that include the current file.
The assisted rename feature (also added in this release), only works for files that are part of a project.
When using a project file, it is no longer necessary to use include directives. In the previous version of Dafny, it was already the case that the Dafny CLI, when passed a Dafny project file, does not require include directives to process the Dafny program. The same now holds for the Dafny IDE when working with Dafny files for which a project file can be found.
If any file in the project is resolved, all files in the project are resolved. Opening a file in a project that's already resolved means the opened file is resolved instantly.
The IDE's memory consumption stays the same regardless of how many files in a project are opened. Without a project, the IDE increases it's memory usage for each open file.
Try out the IDE's project support now by creating an empty dfyconfig.toml file in the root of your project repository.
(#4435)
Prior to generating tests, Dafny now checks the targeted program for any features that test generation does not support or any misuse of test generation specific attributes.
Any such issues are reported to the user.
(#4444)
Added documentation of the generate-tests command to the reference manual (#4445)
When two modules in the same scope have the same name, Dafny now reports an error that contains the location of both modules. (#4499)
The Dafny IDE will now report errors that occur in project files.
The Dafny IDE will now shown a hint diagnostic at the top of Dafny project files, that says which files are referenced by the project.
(#4539)
Bug fixes:
Triggers warnings correclty converted into errors with --warn-as-errors (#3358)
Allow JavaScript keywords as names of Dafny modules (#4243)
Support odd characters in pathnames for Go (#4257)
Allow Dafny filenames compiled to Java to start with a digit (#4258)
Parser now supports files with a lot of consecutive single-line comments (#4261)
Gutter icons more robust (#4287)
Unresolved abstract imports no longer crash the resolver (#4298)
Make capitalization of target Go code consistent (#4310)
Refining an abstract module with a class with an opaque function no longer crashes (#4315)
Dafny can now produce coverage reports indicating which parts of the program are expected to be covered by automatically generated tests.
The same functionality can be used to report other forms of coverage.
(#4325)
Fix issue that would prevent the IDE from correctly handling default export sets (#4328)
Allow function-syntax and other options with a custom default to be overridden in dfyconfig.toml (#4357)
There were two differences between verification in the IDE and the CLI, one small and one tiny, which would only become apparent for proofs that Z3 had trouble verifying. The small difference has been resolved, while the tiny one still persists, so the IDE and CLI should behave almost equivalently now, including resource counts, on most code. (#4374)
Old command line interface for test generation is no longer supported, all calls should use dafny generate-tests (#4385)
Fixed a bug leading to stack overflow during counterexample extraction on some programs. (#4392)
Ability to use .Key as a constant name in datatypes and classes (#4394)
Existential assertions are now printed correctly (#4401)
When a symbol such as a method is not given a name, the error given by Dafny now shows where this problem occurs. (#4411)
Fix flickering and incorrect results in the verification status bar, and improve responsiveness of verification diagnostics (#4413)
Significantly improve IDE responsiveness for large projects, preventing it from appearing unresponsive or incorrect. Previously, for projects of a certain size, the IDE would not be able to keep up with incoming changes made by the user, possibly causing it to never catch up and appearing frozen or showing outdated results. (#4419)
Declarations with {:only} ensure that other declarations aren't displayed as verified in the gutter icons (#4432)
Fix issues that could cause the IDE status bar to show incorrect information (#4454)
When verification times out, only show a red underline on the name of the verifiable for which verification timed out, instead of under its whole definition. (#4477)
Prevent the IDE from becoming completely unresponsive after certain kinds of parse errors would occur. (#4495)
Support all types of options in the Dafny project file (dfyconfig.toml) (#4506)
Fix an issue that would cause some types of errors and other diagnostics not to appear in the IDE, if they appeared in files other than the active one. (#4513)
Fix an IDE issue that would lead to exceptions when using module export declarations and making edits in imported modules that were re-exported (#4556)
Fix a leak in the IDE that would cause it to become less responsive over time. (#4570)

New in Dafny 4.2.0 (Jul 20, 2023)

New features:
The --show-snippets options is implemented for errors printed to the console (#3304)
{:error} now accepts success messages
Better hover messages when using the IDE
Harmonized language to use more "could not prove" rather than "might not hold"
Unicode representations of mathematical symbols (such as logical implies, and, and or) are no longer recognized by the parser. (#3755)
Removed obsolete options /mimicVerificationOf, /allowGlobals (#4062)
Allow the {:only} attribute to be used on members in addition to assert statements (#4074)
The obsolete and unsound option /allocated is removed; the behavior of dafny is locked to the case of /allocated:4. (#4076)
When using the Dafny CLI, error messages of the form "the included file contains error(s)" are no longer reported, since the actual errors for these included files are shown as well. When using the Dafny server, errors like these are still shown, since the Dafny server only shows errors for currently opened files. In addition, such errors are now also shown for files that are indirectly included by an opened file. (#4083)
When using the Dafny IDE, parsing is now cached in order to improve performance when making changes in multi-file projects. (#4085)
Errors issued in command-line mode now show source code context by default; this behavior can be disabled using the option --show-snippets:false. (#4087)
Reduced resolution time by up to 50%. Measurements on large codebases show a 35% average reduction in resolution time.
After generating Python code we run the byte-code compiler to surface possible issues earlier, if it's not subsequently run. (#4155)
Improve the responsiveness of the Dafny language server when making changes while it is in the 'Resolving...' state. (#4175)
It is now possible to reveal an instance function of a class by a static reveal, without the need of an object of that class. (#4176)
Support for the --bprint option for language server arguments (#4206)
Improve printing of real numbers to use decimal notation more often (#4235)
When translated to other languages, Dafny module names no longer have the suffix _Compile appended to them. This may cause issues with existing code from non-Dafny languages in your codebase, if that code was previously referencing modules with _Compile in the name. You can migrate either by removing the _Compile part of references in your codebase, or by using the backwards compatibility option --compile-suffix when using translate, build, or run. (#4265)
Counterexample parsing now supports both the 'Arguments' and 'Predicates' polymorphism encoding in Boogie. (#4299)
Bug fixes:
Removed wrong "related position" precision when dealing with regrouped quantifiers (#2211)
Fixed crash on an empty filename (#3549)
Fixes crash if solver-path is not found (#3572)
Avoid infinite recursion when trying to construct a potentially self-referential object during test generation (#3727)
Better error message when incorrect number of out parameters (#3835)
Compilation of continue labels no longer crashing in Go (#3978)
The terminology 'opaque type' is changed to 'abstract type (for uninterpreted type declarations), to avoid ambiguity with used of the 'opaque' keyword and revealing declarations (#3990)
Ensures override checks have access to fuel constant equivalences (#3995)
No more crash when using constant in pattern (#4000)
Remove multiset cardinality cap in Python (#4014)
Wrong statement order in generated code for certain for-loops (#4015)
Making assertion explicit work for nested statements (#4016)
Use type antecedent in Type/Allocation axioms for const fields
Don't generate injectivity axioms for export-provided types
Added a new CLI option --warn-deprecation, which is on by default
Extraneous semicolons are now warned about by default; the warning can be disabled using --warn-deprecation:false
Regression in the subset check of the function override check (#4056)
Fix function to function-by-method transformation pass in test generation that could previously lead to parsing errors (#4067)
Modules verified in the correct order to prevent Boogie Crash (#4139)
In VSCode, resource units are now always displayed with 3 digit precision.
Moreover, they can now display values greater than MAX_INT without displaying a negative result.
Remove redundant code in the test generation project (#4146)
Generate type axioms in the absence of explicit constraints for newtypes (#4190)
Support for opaque function handles (#4202)
Traits with opaque functions can now be extended without errors (#4205)
Disabled --show-snippets CLI option, which is otherwise on by default, during test generation
Test generation modifies Boogie AST resulting from Dafny, and is, therefore, incompatible with --show-snippets
Select proper division for real-based newtypes (#4234)
Formatting in the IDE consistent again with the CLI (#4269)
Fixes invalid declaration errors when verifying directly from Dafny using /typeEncoding:m. (#4275)
Make gutter icons more robust to document changes (#4308)

New in Dafny 4.1.0 (May 10, 2023)

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
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 an 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
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)

New in Dafny 4.0.0 (Mar 3, 2023)

New in Dafny 3.13.1 (Mar 3, 2023)

New in Dafny 3.13.0 (Mar 2, 2023)

New in Dafny 3.12.0 (Feb 21, 2023)

New in Dafny 3.11.0 (Feb 1, 2023)

Having a library or executable jar simplifies the user's task in figuring out how to use the built artifacts.
Proper warning that 'new' cannot be used in expressions, instead of a parse error.
The attributes :dllimport and :handle are now deprecated. They were undocumented, untested, and not maintained.
Fixed an axiom related to sequence comprehension extraction.
New features:
Go to definition now works reliably across all Dafny language constructs and across files.
Improve performance of Go code by using native byte/char arrays.
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.
Integrate the Dafny auditor plugin as a built-in dafny audit command.
Add the --solver-path option to allow customizing the SMT solver used when using the new Dafny CLI user interface.
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.
For the command translate, renamed the option --target into language and turned it into a mandatory argument.
Havoc assignments now count as assignments for definite-assignment checks. Unless --enforce-determinism is used, no errors are given for arrays that are allocated without being initialized.
Enable passing a percentage value to the --cores option, which will use a percentage of the total number of logical cores on the machine for verification.
Bug fixes:
Nonexistent files passed on the CLI result in a graceful exit.
Check loop invariants on entry, even when such are the only proof obligations in a method.
The :options attribute now accepts new style options --function-syntax and --quantifier-syntax.
Improved error messages for dafny translate.
The :test attribute is now compatible with dafny run and dafny build.
Settings --cores=0 will cause Dafny to use half of the available cores.
Remove an infeasible assertion in the Dafny Runtime for Java.
Language server displays more relevant informations on hovering assertions.
Any (==) inferred for a type parameter of an iterator is now also inferred for the corresponding non-null iterator type.
the otherwise ambiguous program fragment export least predicate is parsed such that least (or greatest) is the export identifier.
The parser generated bad tokens when invoked through /library.
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

New in Dafny 3.10.0 (Dec 16, 2022)

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)

New in Dafny 3.9.1 (Oct 28, 2022)

New in Dafny 3.9.0 (Oct 3, 2022)

New in Dafny 3.8.1 (Sep 1, 2022)

New in Dafny 3.8.0 (Aug 24, 2022)

New in Dafny 3.7.3 (Jul 20, 2022)

New in Dafny 3.7.2 (Jul 14, 2022)

New in Dafny 3.7.0 (Jun 21, 2022)

New in Dafny 3.6.0 (May 11, 2022)

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)

New in Dafny 3.5.0 (Mar 14, 2022)

New in Dafny 3.4.2 (Feb 21, 2022)

New in Dafny 3.4.1 (Feb 15, 2022)

New in Dafny 3.2.0 (Jul 14, 2021)

Language:
Permit as for reference types. For example, the expression a as object can be used to upcast an array a to type object, and o as array<int> can be used to downcast an object o to an integer array. There is a proof obligation that the expression evaluates to a value of the given type.
Introduce is for reference types. For example, if C is a class that extends a trait Tr and t is a variable of type Tr, then t is C says whether or not the dynamic type of t (that is, the allocated type of t) is C. Any type parameters given in the target type must be uniquely determined from the static type of the expression; this maintains type parametricity in the language. Compilation support is provided for the C#, Java, JavaScript, and Go targets.
Arguments to functions, methods, object constructors, and datatype constructors can be passed in not just positionally, but also by naming the parameter. For example, a call might look like GetIceCream(Vanilla, whippedCream := false, cherryOnTop := true).
Allow parameters to be declared with nameonly, which says the parameter is not allowed to be passed in positionally.
Allow parameters to be declared with a default-value expression.
Introduce for loops. For example, you can now write
for i := 0 to a.Length {
print a[i];
Accept attributes in more places (e.g., on loops and cases).
Resolution, type checking, and type inference
Fix method/function override detection.
Fix omitted resolution of some attributes.
Fix crash related to bitvectors.
Verifier:
Fix soundness issue where types were not cardinality-preserving.
Improve/fix issues in matching-pattern expressions.
Remove a matching loop in integer multiplication.
Improve issues in dealing with function values.
Fix bug that caused omission of some precondition checks.
Fix omitted well-formedness checks on modifies and modify.
Fix some malformed Boogie code.
Additional bug fixes.
Compiler:
Compilation to Go sets flag to request pre-module behavior in Go. (In the future, the Go compiler will change to make use of Go modules.)
For C#, fix rewriting of the name Main.
Bug fixes for traits in Go.
Tuple fixes in C++.
Fix construction of large integers in Java.
Fix comparison of some large integers in JavaScript.
For C++, customize g++ warning settings and null printing based on underlying OS.
Documentation:
Some fixes.
IDE:
Upgrade the LSP Implementation of the Language Server.
Tool:
Make timeLimitMultiplier more specific.
Fix and improve pretty printing.
Implementation:
In the compilers, TargetWriter is now named ConcreteSyntax. It has several new features for making it easier to generate well-formatted target code.
Move some files into Verifier folder.
Swap names Join and Meet.

New in Dafny 3.1.0 (Apr 22, 2021)

Language:
feature: Allow invocations of two-state functions/lemmas to indicate which "old state" to use. The syntax is
F@L(args), where F is the name of the function/lemma and L is a dominating label.
feature: Let any type with members refine its members.
Remove deprecated syntax NT(expr) for converting to a newtype NT. The current syntax is expr as NT.
Resolution, type checking, and type inference
fix: Added missing consistency checks for type characterstics ((!new), (00), (0), (==)).
fix: Check that all (ghost and non-ghost) const/var fields have initializers, when needed.
fix: Disallow decreases * on ghost methods.
If a * is used in a decreases or reads clause, no other expressions or *'s are allowed to be listed.
Update type-inference algorithm: meets and joins are now considered before making decisions about arbitrary numeric types.
Verifier:
feature: Expand guessing of decreases clauses for while loops. The new guessing look at sets, multisets, and sequences, and the guesses may be lexicographic tuples. The most useful of these changes is probably that while s != {} gives rise to the guess decreases s.
feature: Improve and expand auto-triggers for collections. Triggers for more expressions are now generated, so there will be fewer "no trigger" warnings. The changes also improve verifier performance for map comprehensions and fix some bugs.
fix: Remove some unintended differences between receiver parameters and ordinary parameters.
Fix encoding of map comprehensions.
Fix issue with labeled heap states.
fix: Detect and report Boogie out-of-resource errors.
Miscellaneous bug fixes
Compiler:
Fix initialization of let-such-that bound variables.
C#: Fix initialization issues related to extern opaque types.
Java: Fix compilation of datatype constructors with only ghost parameters, and other issues.
Java: Upon javac compilation failure, exit but don't crash.
Go: Fix compilation of map update.
C++: Support tuples with arbitrary arity.
C++: Fix some path-related problems.
Documentation:
Minor improvements and fixed typos
Tool:
feature!: Add command-line option /stdin that reads standard input as if it were a .dfy file. Remove the old support for this, which had been to mention stdin.dfy on the command line.
feature: Apply timeLimitMultipler to rlimit.
Fix/improve some scripts
Implementation:
Merge Language Server sources. This will help us better keep versions and refactorings in synch.
refactor: Improve UserDefinedType AST nodes by removing .ResolvedParam, and related changes.
Miscellaneous:
Various bug fixes throughout

New in Dafny 3.0.0 (Feb 3, 2021)

New in Dafny 3.0.0 Pre-release 0 (Aug 18, 2020)

Language:
Allow datatype, codatatype, and newtype types to declare members (just like a class and a trait can declare members).
Introduce :- statements and expressions.
This new assignment operator extracts a successful value from the right-hand side (RHS) of the assignment, or propagates a failure if the evaluation of the RHS reports a failure. Some examples are in Test/exceptions/Exceptions1.dfy and Test/exceptions/Exceptions1Expressions.dfy.
Introduce expect statements.
The statement expect E, V; checks boolean expression E at run time and halts execution if it evaluates to false. The optional argument V is used in the error message produced. The verifier treats the statement as assume E;.
Introduce :- expect (a.k.a. assign-or-halt) statements.
This variation of the :- halts execution if the RHS reports a failure. Some examples are in Test/expectations/ExpectAndExceptions.dfy.
Traits and classes that extend traits can now have type parameters.
All occurrences of a trait among the ancestor traits of a class (or trait) must have the same type-parameter instantiations.
Traits can now extend other traits.
Order the cases of match statements/expressions.
This allows overlaps between cases, where an earlier case gets selected first. A case can now also be just a variable (or _), which in effect is an "else". (Note, this is a backward compatible change, since no overlaps among cases were allowed before.) A warning is generated if one case is already covered by the preceding cases.
Patterns in match cases can now use simple literal expressions, such as 2, 3.14, and false.
Add full verification support for body-less loops.
The loop targets of such a loop are the free mutable variables (including the heap) that occur in the guard, invariant, or decreases clause. If the loop has a modifies clause--whatever the modifies clause says--then the heap is counted as a loop target.
Breaking change: In an export declarations, members of types are exported separately from exporting the type.
to export a member, the enclosing type must be provided or revealed
class constructors and mutable fields can be exported only if the enclosing class/trait is revealed
mutable fields can no longer be revealed, only provided
datatype constructors, discriminators, and destructors are exported when the datatype is revealed, and can never be explicitly named in exports
for an extreme predicate/lemma, the corresponding prefix predicate/lemma is exported, too
Breaking change: New rules for exporting classes.
To reveal a class or trait C will export:
the fact that this is a reference type
both types C and C?, and the connection between these two
the anonymous constructor, if C is a class and has one
To provide a class or trait C will export:
the name C, as an opaque type
not type C?
no constructor or mutable field, and it's an error to explicitly name these in exports
One breaking-change consequence of these rules is that constructor-less new is no longer supported for imported classes.
The syntactic form import A.B.C is now allowed, and it stands for import C = A.B.C.
import A.B.C`Xis now allowed.
Introduce sequence construction expressions.
Some examples are in Test/dafny0/Comprehensions.dfy.
const fields are not allowed in back-tick notation in frames
Allow import opened A where module A is in the same scope.
Breaking change: Remove support for some deprecated syntax, and removed the keywords array1 and array1?.
Breaking change: Make {: a token instead of two separate tokens.
Breaking change: Disallow modify statements in forall statements.
Breaking change: Don't support map disjointness, that is, a !! b is no longer supported when a and b are maps.
Verifier:
Improve representation of heap (as a map of map, rather than as 2-dimensional map).
Fix refinement checks for two-state predicates.
Don't re-verify code that comes from DLLs.
Compiler:
Add compiler to Java (fully featured, except iterator is not supported).
Add initial version of a compiler to C++.
Add support for {:test} attribute (C# only for now), mapping it to [Xunit.Fact]. This allows xUnit-like unit testing from Dafny.
Compile forall statement into simple loop when possible.
Compile tail-recursive functions (not just tail-recursive methods) with tail calls. For functions, the compiler has an auto-accumulator feature that automatically detects cases when an added accumulator variable allows the function to be transformed into being tail-recursive. In such detected cases, the compiler introduces the accumulator variable automatically.
Enlarged support of {:extern} declarations
Allow the compilation of collection types that take traits as type parameters.
Compile methods with exactly one out-parameter to the usual result-type methods
Compile map comprehensions with multiple bound variables.
Support {:nativeType XX} where XX is a list of native types. They are considered in order and the first one supported by the compiler is picked. An error is generated if the type cannot be determined to fit in that native type. (See the /attrHelp message for details.) Also, number is no longer supported outside JavaScript.
The .NET immutable collections that used to be used with the /optimize flag are now always used. The System.Collections.Immutable.dll library is no longer part of the Dafny distribution, since it is part of .NET. Also, /optimize flag is now permanently on, which causes /optimize flag to be passed down to the C# compiler.
Introduce branch-coverage profiling. See new /coverage flag.
Improved formatting of target code
Breaking change: A number of features are now represented different at run time. This may break any previous external code that depended on the old representations.
Documentation:
Updates to the Dafny Language Reference Manual.
For Dafny contributors, added documentation of compilation of trait/class to C#/Java/JavaScript/Go.
IDE:
End support of the DafnyExtension, which was the original Dafny IDE that plugged into Microsoft Visual Studio. (VS Code and Emacs plug-ins are still supported.)
Miscellaneous:
Various bug fixes throughout

New in Dafny 2.3.0 (May 7, 2019)

Language:
Datatype updates are now allowed to update shared destructors. However, updates are now restricted to those that don't change the value's constructor. Also, updates where a candidate result constructor has anonymous parameters are no longer allowed. A precise description of datatype update is found in Test/dafny0/SharedDestructors.dfy, starting at line 65. Improved error messages and /rprint option for datatype updates.
Added labeled assertion statements and labeled method/iterator preconditions. The syntax is like assert L: Expr; and requires L: Expr. The assumption that usually comes from an assertion or precondition is suppressed when these are labeled. To use the assumption, a reveal L; statement or expression must be used.
See Test/dafny3/CalcExample.dfy for some examples.
Labels, both in the statement label L: and in the new labeled assertions and preconditions, are now allowed to look like numeric literals (as was already allowed for field names and datatype destructors).
reveal statements can now take a list of arguments.
Allow more types with non-0 initializers to be passed as type parameters (supported by the compiler's
new use of run-time type descriptors).
Allow a module's submodules to be given in separate files: A module can now be declared with a qualified name. This is a just a syntactic shorthand for inserting the module into the indicated parent module. For example,
module A {
module B { }
must be written in one file, or else the curly braces won't match up. But these declarations can now be provided as:
module A { }
module A.B { }
which allows A and A.B to be declared in separate files.
A non-abstract module is not allowed to import or use (as in dereferencing the name of) an abstract module. However, any non-abstract module is allowed to contain or refine abstract modules.
Type checking
Temporarily, added a {:termination false} attribute that can be placed on trait declarations to unsoundly ignore termination checking for dynamic method dispatch that goes to other modules. A better and sound solution will come in the future.
Various bug fixes
Verifier:
Added specialized (extensional) equality for inductive datatypes.
Various bug fixes
Compiler:
Compilation now targets not just .NET (via C#), but also JavaScript and Go. These are selected with the command-line switch /compileTarget:<language>, where <language> is one of cs, js, or go.
For compilation to JavaScript, also accept files with extension .js on the command line.
Improved {:extern} for methods and function:
{:extern} says to use the Dafny method name as the external name.
{:extern "M"} and {:extern "Q", "M"} say to use M as the external name.
In the 0- and 1-argument forms, qualified forms of the method name are constructed according
to the enclosing class and modules in Dafny (and those enclosing declarations may have
:extern attributes themselves, which are be taken into account).
In the 2-argument form, Q.M is used as the qualified name and the names of enclosing classes
and modules are not consulted. If needed, Q can contain dots; for example,
{:extern "R.S.T", "M"} will cause the qualified name of the extern to be R.S.T.M.
An {:extern} constructor is now called using C#'s constructor mechanism.
Improved {:extern} for modules:
{:extern} says to use the module name as the extern name.
{:extern "N"} says to use "N" as the extern name.
{:extern "N", "L"} for JavaScript says to use "N" as the extern name and to initialize it to
require("L").
For compilation to Go, {:extern ""} indicates Go's built-in "module", which contains types
like error. (For more information about using externs with Go, see Docs/Compilation/Go.md.)
Support for interacting with C code on .NET. The {:dllimport} attribute translates to the .NET DllImportAttribute. Attribute {:handle} can be placed on some reference types to cause their translation to turn into uninterpreted machine words.
Deprecated extern keyword. Use the {:extern} attribute instead.
Allow program entry point (Main method) to take any number of ghost in- and out-parameters.
Added command-line option /compile:4, which is like /compile:3 but compiles/runs regardless of how the verification turned out.
Added command-line option /compileVerbose, which can suppress some information compiler output.
Removed the struct that was previously used in the C# compilation of datatypes. Also, compilation of datatypes with only one constructor are special-cased.
Renamed tuple types in the compiled code to something more straightforward and human readable.
Improvements in identifier-protection schemes (which avoid clashes with keywords in the target language).
Compilation to C# uses /nowarn:0168 to suppress warnings about unused variables under Mono.
Improved printing of real numbers.
Various improvements in compiled code.
Various bug fixes

New in Dafny 2.2.0 (Sep 24, 2018)

New in Dafny 2.1.1 (Sep 24, 2018)

Language:
Introduced old@L(expr) and unchanged@L(frame_expr) expressions, which can refer to the value of the heap at an indicated statement label L.
Labels, functions, and methods can now, like fields and (co)datatype destructors, have names that look like numeric integer literals.
Duplicate labels are no longer allowed when one of the labels dominates the other.
The continuity restriction for (co)inductive predicates has been relaxed. More precisely, there is no requirement of continuity for (co)inductive predicates using [ORDINAL] (which is also the default). The restriction applies only to predicates explicitly declared with [nat].
Abstemious functions: Allow functions to be annotated with {:abstemious}. Such a function is checked not to consume too much. More precisely, an abstemious function can only codatatype-destruct parameters and must return with a co-constructor.
Abstemious functions, together with a new computation of a guaranteed minimum number of co-constructor wrappers, expand the number of functions that are considered to be productive. As a result, many new interesting co-recursive functions can be written.
When appropriate, try to give a hint about declaring a function to be abstemious.
Fewer restrictions on quantifiers over ORDINAL. Such quantifiers are now restricted only in the definition of (co)inductive predicates.
Verifier:
More precise computations of when the heap is being used. This makes some logical encodings more efficient.
More knowledge about the exhaustive set of constructors of (co)datatypes. In particular, the new knowledge springs into being whenm two (co)datatype values are compared with equality or disequality. This makes it easier to prove programs that do direct comparisons rather than using a match construct.
IDEs:
Make DafnyServer use the same version number as Dafny. This enable the Dafny plug-in for VS Code to accurately figure out when to offer to download the newest version of Dafny.
Build:
Updated the Coco build and .exe to use VS 2017 and a .NET version 4.5
Miscellaneous:
Some bugs fixes.

New in Dafny 2.1.0 (Feb 9, 2018)

Language:
Non-null types.
A declaration of a class or trait C gives rise to two types, C? and C.
Type C? is the possibly null reference type for C objects. Previously in Dafny, this was the only type the class or trait gave rise to and it then had the different name C.
Type C is a non-null version of C?. It is a defined as the subset type:
type C = c: C? | c != null
Note that the ? is part of the name of the class C?. It is not a suffix operator, so there cannot be any space between the C and the ?. Also, if a class C has type parameters, then these are mentioned after the type names C? and C, for example, C?<int> and C<int>.
In some places in the program text, a class or trait name is expected. In particular, a trait name is expected after the extends keyword in a class declaration and a class name is expected in a new allocation. Note that these names, because they are class and trait names, not type names, do not end with a ?.
Dafny has a built-in trait object and any number of built-in array classes (array, array2, array3, ...). Each of these also gives rise to two types, as in object? and object, array? and array, array2? and array2, etc.
If the literal null is compared with an expression of a non-null type, Dafny will emit a warning that the result of the test can be determined at compile time. For example, if p has a non-null type and S is a set whose element type is a non-null type, then both p != null and null in S will generate said warning.
The subset types declared in a program form a hierarchy (that is, a tree), where the parent of a subset type is its given base type. This hierarchy is part of the subtype relation in Dafny. For example, nat is a subtype of int, and for any class or trait C, C is a subtype of C?. In addition, for every class or trait C that extends a trait Tr, type C? is a subtype of Tr? and type C is a subtype of Tr.
As a consequence of these rules, note that the subtype relation is not just a hierarhcy.
Suppose X is a subset type whose base type is C. It then follows that X is a subtype of C, which in turn is a subtype of C?. However, the declaration of X only gives rise to one type. In particular, it does not also give rise to a type X?. In other words, any user-defined subset type of C? or C is only a subtype of it.
Type inference is now more precise. Whereas before it would not infer subset types like nat or --> (but instead their base type, int and ~>), now it will try to infer such types. In some cases, this will not make a noticeable, but there are two cases where the difference may be important.
One case is that type arguments more easily will be inferred as subset types. For example, suppose the usual datatype List has a co-variant type parameter and suppose xs is a variable declared to have type List<nat>. Expression Cons(55, xs) may now be inferred to have type List<nat> as well. This is beneficial for verification, because in an assignment like xs := Cons(55, xs);, the verifier only needs to check that 55 satisfies the constraint of nat. Previously, it was more likely that Cons(55, xs) would be inferred to have type List<int>, in which case the assignment xs := Cons(55, xs); put the burden on the verifier to check that Cons(55, xs) produces a value that actually satisfies List<nat>.
The other case where the more precise type inference can make a noticeable difference is in comprehensions like quantifications and set comprehensions. Suppose P is a predicate declared to take a parameter of type nat and consider an expression forall x :: P(x) ==> 0 <= x. If x has type nat, then this quantifier is a tautology. If x has type int, then the expression is not well-formed, because the subexpression P(x) would not satisfy the type conditions of P. For this example, Dafny will infer the type of x to be nat.
As another example, of a quantifier, suppose P and Q are both predicates that take a nat argument. Then, Dafny will infer x to have type nat in forall x :: 0 <= x && P(x) ==> Q(x) as well. So, in this example, since x is inferred to be of type nat, the antecedent 0 <= x is redundant and can be omitted.
As a third example, suppose neg is a subset type of int that stands for the negative integers, P is a predicate that takes an argument of type nat, and Q is a predicate that takes an argument of type neg. Consider the following expression:
forall x :: (0 <= x ==> P(x)) && (0 < x ==> Q(x))
For this expression, Dafny will infer that x has type int. In an alternative design, inference might have resulted in the type nat or neg, each of which would render one of the conjuncts trivially satisfied, or resulted in error message like "overconstrained type".
Allow more RHSs of const declarations.
The possible variance indicators on type parameters has been expanded. The possibilities are:
+ (co-variance, strict)
Enclosing type is monotonic in the type parameter.
The parameter is not used in expanding positions (that is, it is not used left of any arrow).
* (co-variance, relaxed)
Enclosing type is monotonic in the type parameter.
Other than that, use of the parameter is unrestricted (in particular, it may be used to the left of an arrow).
(default variance, denoted by not giving any of the other variance indicators explicitly) (non-variance, strict)
Different given parameters produce non-comparable types.
The parameter is not used in expanding positions (that is, it is not used left of any arrow).
! (non-variance, relaxed)
Different given parameters produce non-comparable types.
Other than that, use of the parameter is unrestricted (in particular, it may be used to the left of an arrow).
- (contra-variance)
Enclosing type is anti-monotonic in the type parameter.
Consequentially, every use of the parameter is to the left of some arrow.
Strict positivity is used to forbid type definitions where differences in cardinalities would give rise to a logical contradiction.
Added type-parameter characteristic (!new), which says that the type does not include any references, and thus does not depend on the allocation state. It can be used to restrict type parameters so that functions can use the type in unbounded quantifications.
Opaque types at the very topmost scope are always implicitly (!new).
Verification:
Support for customizable error messages (useful for tools built on top of Dafny).
Removed the notoriously bad seq axiom. (More precisely, rewrote it to have a good trigger.)
Some performance improvements.
Improved and expanded on the syntactic bounds discovery in comprehensions.
IDE:
Visual Studio mode is for VS 2017
Compiler:
Some bug fixes, for example to work around some questionable designs around the use of null in the .NET collection libraries.
Command-line options
Command-line option /titrace spills out debug trace information from the type inference process. Previously, this debug trace information was hidden under an #if, but now it can be turned on without having to recompile Dafny.
Added /noExterns flag, which ignores :extern attributes.
Started implementing a /allocated:4 mode.
Miscellaneous:
Include Code Contracts for VS 2017. This requires Code Contracts to have been installed (for some version of Visual Studio, like VS 2015) on the machine.
Various bug fixes.

New in Dafny 1.9.5 (May 11, 2015)

New in Dafny 1.9.4 (May 11, 2015)

Semi-colons are no longer needed at the end of specification clauses (like `requires`, `invariant`). Semi-colons are now required only as statement terminators, as terminators of lines in `calc` statements, in let expressions, and in statement expressions.
Names are now resolved in a different order, from local out to the module scope.
Type arguments can be user specified (using angle brackets after the name of the function or method).
Functions and methods declared at the module level are now automatically declared as static. In fact, the `static` keyword is no longer allowed to be placed on such functions and methods. With this change, fields are no longer allowed to be declared at the module level. (The `/allowGlobals` command-line switch can help with the transition from old code to new code where such fields are to be declared inside user-declared classes.)
Previously, functions were opaque outside the declaring module. That is, the body of a function was hidden from outside the module. This is no longer the case. To make a function opaque (both inside and outside the declaring module), use the `:opaque` attribute. The body can then be revealed using the corresponding `reveal_` lemma. To prevent the body from ever being revealed outside the declaring module, use the new `protected` modifier on the function.
A class can now extend multiple traits.
In addition to the finite-map type `map`, there is now also a map type whose domain can be infinite: `imap`.
A `newtype` that can fit into a native integral type now gets compiled into the smallest such type. This behavior can be customized by the `:nativeType` attribute.
Let-such-that expressions (aka Hilbert's epsilon operator) are now allowed in non-ghost code, provided they prescribe a unique value (as is checked by the verifier). (This restriction means that compiled let-such-that expressions really correspond to Hilbert's iota operator.)
Improvements in the fine-grained caching in the Dafny IDE. This caching is now turned on by default.
As the Dafny IDE starts up, it will read command-line options from a new file called `DafnyOptions.txt` in the .vsix plug-in directory.
The old vim mode for Dafny has been replaced by the vim-loves-dafny package.
`:trigger` attributes can now be used also in let and let-such-that expressions, in set, map, and imap comprehensions, and in assign-such-that statements.
Attribute `:timeLimitMultiplier` can be used as an alternative to `:timeLimit`. It computes a time limit as the product of the `/timeLimit` on the command line and the given multiplier.
Many bug fixes

New in Dafny 1.9.1 (Oct 21, 2014)

Language changes that break backward compatibility:
Declarations and invocations of nullary predicates now require parentheses (to distinguish invocations from using the predicate as a first-class function value)
Stricter rules for ambiguously specified types (may require additional manually supplied types, since type inference may now in some cases do less)
Function "reads" clauses now need to frame themselves and preconditions
Changed behavior of "decreases * ". To use "decreases * ", the enclosing context must also allow "decreases * ". (Consequently, note that "decreases * " is now allowed on any method, not just on tail recursive methods, which increases the chance that non-terminating methods may run out of stack space.) Also, "decreases * " is now inherited in refining modules.
Type conversion from "real" to "int" no longer does truncation, but instead is defined only if the "real" has no fractional part. To truncate a "real", use the new ".Trunc" member.
Identifier names are no longer allowed to contain backslashes
New language features:
First-class functions (higher-order functions), lambda expressions
"newtype" declaration for user-defined numeric types
Built-in tuple types and tuples
Traits (abstract superclasses), basic features
Types "char" and "string" (this is the difference between version 1.9.0 and version 1.9.1)
User-defined type synonyms
Opaque types can now take type parameters
Syntax for "match" expressions and "match" statements the same --- curly braces around the cases are now supported for both and are optional for both
Change in scoping to allow a datatype to have a constructor with the same name.
Auto-declaration of type parameters used in signatures
Type parameters for arrays and collection types can now be filled in automatically in signatures
Datatype rank comparison, written " set"
Improvements in verification:
Computations can now also include sequences and lambda literals
Improved triggering in "forall" assignment statements
Command-line support for verifying snapshots
New logical encoding of types, supporting type parameters properly
Dafny IDE enhancements:
Now works in both Visual Studio 2012 and Visual Studio 2013
Advanced caching of verification results
Compilation output is now display in the Visual Studio Output pane
Shorter wait-for-idle time

Dafny Changelog

What's new in Dafny 4.6.0

New in Dafny 4.5.0 (Mar 16, 2024)

New in Dafny 4.3.0 (Sep 29, 2023)

New in Dafny 4.2.0 (Jul 20, 2023)

New in Dafny 4.1.0 (May 10, 2023)

New in Dafny 4.0.0 (Mar 3, 2023)

New in Dafny 3.13.1 (Mar 3, 2023)

New in Dafny 3.13.0 (Mar 2, 2023)

New in Dafny 3.12.0 (Feb 21, 2023)

New in Dafny 3.11.0 (Feb 1, 2023)

New in Dafny 3.10.0 (Dec 16, 2022)

New in Dafny 3.9.1 (Oct 28, 2022)

New in Dafny 3.9.0 (Oct 3, 2022)

New in Dafny 3.8.1 (Sep 1, 2022)

New in Dafny 3.8.0 (Aug 24, 2022)

New in Dafny 3.7.3 (Jul 20, 2022)

New in Dafny 3.7.2 (Jul 14, 2022)

New in Dafny 3.7.0 (Jun 21, 2022)

New in Dafny 3.6.0 (May 11, 2022)

New in Dafny 3.5.0 (Mar 14, 2022)

New in Dafny 3.4.2 (Feb 21, 2022)

New in Dafny 3.4.1 (Feb 15, 2022)

New in Dafny 3.2.0 (Jul 14, 2021)

New in Dafny 3.1.0 (Apr 22, 2021)

New in Dafny 3.0.0 (Feb 3, 2021)

New in Dafny 3.0.0 Pre-release 0 (Aug 18, 2020)

New in Dafny 2.3.0 (May 7, 2019)

New in Dafny 2.2.0 (Sep 24, 2018)

New in Dafny 2.1.1 (Sep 24, 2018)

New in Dafny 2.1.0 (Feb 9, 2018)

New in Dafny 1.9.5 (May 11, 2015)

New in Dafny 1.9.4 (May 11, 2015)

New in Dafny 1.9.1 (Oct 21, 2014)

New in Dafny 1.8.2 (Apr 23, 2014)

New in Dafny 1.8.1 (Mar 26, 2014)

New in Dafny 1.8.0 (Jan 16, 2014)

New in Dafny 1.7.0 (Aug 12, 2013)