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

• Documenting Dafny Entities

  • 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-runtime 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)

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

Dafny 3.13.1

Bug fixes

• Restore publishing language server to nuget
• Fix allow_on_mac.sh for z3 paths

Dafny 3.13.0

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)

Dafny 3.12.0

New features

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

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

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

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

Dafny 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

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