Dafny Versions Save

New features

• Go to definition now works reliably across all Dafny language constructs and across files. (https://github.com/dafny-lang/dafny/pull/2734)

• Improve performance of Go code by using native byte/char arrays (https://github.com/dafny-lang/dafny/pull/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. (https://github.com/dafny-lang/dafny/pull/3061)

• Integrate the Dafny auditor plugin as a built-in dafny audit command. (https://github.com/dafny-lang/dafny/pull/3175)

• Add the --solver-path option to allow customizing the SMT solver used when using the new Dafny CLI user interface. (https://github.com/dafny-lang/dafny/pull/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. (https://github.com/dafny-lang/dafny/pull/3185)

• For the command translate, renamed the option --target into language and turned it into a mandatory argument. (https://github.com/dafny-lang/dafny/pull/3239)

• Havoc assignments now count as assignments for definite-assignment checks. (https://github.com/dafny-lang/dafny/pull/3311)

• Unless --enforce-determinism is used, no errors are given for arrays that are allocated without being initialized. (https://github.com/dafny-lang/dafny/pull/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. (https://github.com/dafny-lang/dafny/pull/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. (https://github.com/dafny-lang/dafny/pull/3355)

Bug fixes

• Nonexistent files passed on the CLI now result in a graceful exit (https://github.com/dafny-lang/dafny/pull/2719)

• Check loop invariants on entry, even when such are the only proof obligations in a method. (https://github.com/dafny-lang/dafny/pull/3244)

• The :options attribute now accepts new style options --function-syntax and --quantifier-syntax (https://github.com/dafny-lang/dafny/pull/3252)

• Improved error messages for dafny translate (https://github.com/dafny-lang/dafny/pull/3274)

• The :test attribute is now compatible with dafny run and dafny build (https://github.com/dafny-lang/dafny/pull/3275)

• Settings --cores=0 will cause Dafny to use half of the available cores. (https://github.com/dafny-lang/dafny/pull/3276)

• Removed an infeasible assertion in the Dafny Runtime for Java (https://github.com/dafny-lang/dafny/pull/3280)

• Language server displays more relevant information on hovering assertions (https://github.com/dafny-lang/dafny/pull/3281)

• Any (==) inferred for a type parameter of an iterator is now also inferred for the corresponding non-null iterator type. (https://github.com/dafny-lang/dafny/pull/3284)

• The otherwise ambiguous program fragment export least predicate is parsed such that least (or greatest) is the export identifier (https://github.com/dafny-lang/dafny/pull/3291)

• The parser no longer generates bad tokens when invoked through /library (https://github.com/dafny-lang/dafny/pull/3301)

• Match expressions no longer incorrectly convert between newtypes and their basetype (https://github.com/dafny-lang/dafny/pull/3333)

• Warn that 'new' cannot be used in expressions, instead of throwing a parse error (https://github.com/dafny-lang/dafny/pull/3366)

• The attributes :dllimport and :handle are now deprecated. They were undocumented, untested, and not maintained. (https://github.com/dafny-lang/dafny/pull/3399)

• Fixed an axiom related to sequence comprehension extraction (https://github.com/dafny-lang/dafny/pull/3411)

New features

• Emit warnings about possibly missing parentheses, based on operator precedence and unusual identation (https://github.com/dafny-lang/dafny/pull/2783)

• The DafnyRuntime NuGet package is now compatible with the .NET Standard 2.0 and .NET Framework 4.5.2 frameworks. (https://github.com/dafny-lang/dafny/pull/2795)

• Counterexamples involving sequences present elements in ascending order by index. (https://github.com/dafny-lang/dafny/pull/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. (https://github.com/dafny-lang/dafny/pull/3016)

• dafny run now consistently requests UTF-8 output from compiled code. Use chcp 65501 if you see garbled output on Windows. (https://github.com/dafny-lang/dafny/pull/3049)

• feat: support for traits as type arguments by fully allowing variance on datatypes in Java (https://github.com/dafny-lang/dafny/pull/3072)

Bug fixes

• Function by method with the same name as a method won't crash resolver (https://github.com/dafny-lang/dafny/pull/2019)

• Better reporting if 'this' used in a subset type - and no crash (https://github.com/dafny-lang/dafny/pull/2068)

• Support for aliases in module resolution without crashing on imports (https://github.com/dafny-lang/dafny/pull/2108)

• Added missing check to prevent crash during resolution (https://github.com/dafny-lang/dafny/pull/2111)

• No more resolver crash on pattern match with incompatible types (https://github.com/dafny-lang/dafny/pull/2139)

• Refinements get errors at the correct place in LSP (https://github.com/dafny-lang/dafny/pull/2402)

• Resolution errors in the left-hand sign of an assign-such-that statement do not crash Dafny anymore (https://github.com/dafny-lang/dafny/pull/2496)

• old() cannot be inferred as a trigger alone (https://github.com/dafny-lang/dafny/pull/2593)

• Labels are no longer compiled in the case of variable declarations (https://github.com/dafny-lang/dafny/pull/2608)

• No more mention of reveal lemmas when implementing opaque functions in traits (https://github.com/dafny-lang/dafny/pull/2612)

• Verification of abstract modules not duplicated when imported (https://github.com/dafny-lang/dafny/pull/2703)

• Dafny now compiles functions that mix tail- and non-tail-recursive calls without crashing (https://github.com/dafny-lang/dafny/pull/2726)

• substitution of binding guards does not crash if splits present (https://github.com/dafny-lang/dafny/pull/2748)

• No more crash when constraining type synonyms (https://github.com/dafny-lang/dafny/pull/2829)

• Returning a tuple when it should be two variables does not crash Dafny anymore (https://github.com/dafny-lang/dafny/pull/2878)

• Default generic values no longer cause compilation error (https://github.com/dafny-lang/dafny/pull/2885)

• Now publishing Dafny Binary for MacOS Arm64 architecture (https://github.com/dafny-lang/dafny/pull/2889)

• Added a missing case in the Translator (pattern matching for variable declarations) (https://github.com/dafny-lang/dafny/pull/2920)

• The Python and Go backends now encode non-ASCII characters in string literals correctly (https://github.com/dafny-lang/dafny/pull/2926)

• Added a missing case of TypeSynonymDecl in the resolver that caused a crash (https://github.com/dafny-lang/dafny/pull/2927)

• Fix malformed Boogie generated for extreme predicates (https://github.com/dafny-lang/dafny/pull/2984)

• Counter-examples with non-integer sequence indices do not crash Dafny anymore. (https://github.com/dafny-lang/dafny/pull/3048)

• Use correct type for map update expression (https://github.com/dafny-lang/dafny/pull/3059)

• Language server no longer crashing in special case (https://github.com/dafny-lang/dafny/pull/3062)

• Resolved an instance in which the Dafny language server could enter a broken state. (https://github.com/dafny-lang/dafny/pull/3065)

• Do not refer to an implicit assignment in error messages on return statements (https://github.com/dafny-lang/dafny/pull/3125)

• Multiple exact same failing assertions do not crash the Boogie counter-example engine anymore (https://github.com/dafny-lang/dafny/pull/3136)

• Duplicate declarations caused by resolver do not crash the language server anymore (https://github.com/dafny-lang/dafny/pull/3155)

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. (https://github.com/dafny-lang/dafny/pull/2820)

Bug fixes

• Correct error highlighting on function called with default arguments (https://github.com/dafny-lang/dafny/pull/2826)

• Crash in the LSP in some code that does not parse (https://github.com/dafny-lang/dafny/pull/2833)

• A function used as a value in a non-ghost context must not have ghost parameters, and arrow types cannot have ghost parameters. (https://github.com/dafny-lang/dafny/pull/2847)

• Compiled lambdas now close only on non-ghost variables (https://github.com/dafny-lang/dafny/pull/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. (https://github.com/dafny-lang/dafny/pull/2876)

• Handle sequence-to-string equality correctly in the JavaScript runtime (https://github.com/dafny-lang/dafny/pull/2877)

• don't crash on type synonyms and subset types of array types in LHSs of simultaneous assignments (https://github.com/dafny-lang/dafny/pull/2884)

• Removed an bogus optimization on the Language Server (https://github.com/dafny-lang/dafny/pull/2890)

• The Dafny-to-Java compiler will now fully-qualify type casts in pattern destructors, avoiding "reference to TYPE is ambiguous" errors from javac. (https://github.com/dafny-lang/dafny/pull/2904)

• Variable declarations and formals in match cases do not trigger errors anymore. (https://github.com/dafny-lang/dafny/pull/2910)

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

• feat: Support for the {:opaque} attibute on const (https://github.com/dafny-lang/dafny/pull/2545)
• feat: Support for plugin-based code actions on the IDE (https://github.com/dafny-lang/dafny/pull/2021)
• fix: Fixed a crash when parsing newtype in the parser (https://github.com/dafny-lang/dafny/pull/2649)
• fix: Added missing error reporting position on string prefix check (https://github.com/dafny-lang/dafny/pull/2652)
• fix: Prevent LSP server from exiting when a crash occurs (https://github.com/dafny-lang/dafny/pull/2664)
• fix: Fix bug where LSP server would not show diagnostics that referred to included files (https://github.com/dafny-lang/dafny/pull/2664)
• fix: Check all compiled expressions to be compilable (https://github.com/dafny-lang/dafny/pull/2641)
• fix: Better messages on hovering failing postconditions in IDE (https://github.com/dafny-lang/dafny/pull/2654)
• fix: Better error reporting on counter-examples if an option is not provided (https://github.com/dafny-lang/dafny/pull/2650)

• fix: Use the right bitvector comparison in decrease checks (https://github.com/dafny-lang/dafny/pull/2512)
• fix: Don't use native division and modulo operators for non-native int-based newtypes in Java and C#. (https://github.com/dafny-lang/dafny/pull/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. (https://github.com/dafny-lang/dafny/pull/2448)
• feat: The Dafny Language Server used by the VSCode IDE extension is now available as a NuGet package called DafnyLanguageServer (https://github.com/dafny-lang/dafny/pull/2600)
• fix: Counterexamples - fix an integer parsing bug and correctly extract datatype and field names (https://github.com/dafny-lang/dafny/pull/2461)
• feat: New option -diagnosticsFormat:json to print Dafny error messages as JSON objects (one per line). (https://github.com/dafny-lang/dafny/pull/2363)
• fix: No more exceptions when hovering over variables without type, and types of local variabled kept under match statements (https://github.com/dafny-lang/dafny/pull/2437)
• fix: Check extreme predicates and constants in all types, not just classes (https://github.com/dafny-lang/dafny/pull/2515)
• fix: Correctly substitute type variables in override checks (https://github.com/dafny-lang/dafny/pull/2522)
• feat: predicate P(x: int): (y: bool) ... is now valid syntax (https://github.com/dafny-lang/dafny/pull/2454)
• fix: Improve the performance of proofs involving bit vector shifts (https://github.com/dafny-lang/dafny/pull/2520)
• fix: Perform well-definedness checks for ensures clauses of forall statements (https://github.com/dafny-lang/dafny/pull/2606)

• 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. (https://github.com/dafny-lang/dafny/pull/2434)
• feat: Whitespaces and comments are kept in relevant parts of the AST (https://github.com/dafny-lang/dafny/pull/1801)
• fix: NuGet packages no longer depend on specific patch releases of the .NET frameworks.

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

This is an automatically published nightly release. This release may not be as stable as versioned releases and does not contain release notes.

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. (https://github.com/dafny-lang/dafny/pull/2277)