dafny-lang/dafny v3.10.0

Dafny 3.10.0

on GitHub

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)