Dafny 3.10.0

[alex-chew]

New features

• Emit warnings about possibly missing parentheses, based on operator precedence and unusual identation (Add warnings about possibly confused operator precedence #2783)

• The DafnyRuntime NuGet package is now compatible with the .NET Standard 2.0 and .NET Framework 4.5.2 frameworks. (Build DafnyRuntime for netstandard2.0 and net452 instead of net6.0 #2795)

• Counterexamples involving sequences present elements in ascending order by index. (Counterexamples involving seqs should present elements ordered 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.
  (feat: Unicode strings (--unicode-char) #3016)

• dafny run now consistently requests UTF-8 output from compiled code.
  Use chcp 65501 if you see garbled output on Windows.
  (feat: Make sure that dafny run always requests UTF-8 encoded output #3049)

• feat: support for traits as type arguments by fully allowing variance on datatypes in Java (feat: support for traits as type arguments with variance on datatypes in Java #3072)

Bug fixes

• Function by method with the same name as a method won't crash resolver (function-by-method crash #2019)

• Better reporting if 'this' used in a subset type - and no crash (Resolver crash #2068)

• Support for aliases in module resolution without crashing on imports (Crash in ModuleQualifiedId.Set #2108)

• Added missing check to prevent crash during resolution (Assertion failure in ResolveDotSuffix #2111)

• No more resolver crash on pattern match with incompatible types (Crash in Resolver.CheckLinearExtendedPattern #2139)

• Refinements get errors at the correct place in LSP (Crash on refinement #2402)

• Resolution errors in the left-hand sign of an assign-such-that statement do not crash Dafny anymore (NullReferenceException crash in ErrorReporter.Error due to Resolver.CheckIsLvalue #2496)

• old() cannot be inferred as a trigger alone (Malformed triggers #2593)

• Labels are no longer compiled in the case of variable declarations (JavaScript compiler and labels issue #2608)

• No more mention of reveal lemmas when implementing opaque functions in traits (Reveal lemmas are not copied from traits to extending classes, leading to resolution errors #2612)

• Verification of abstract modules not duplicated when imported (Dafny reports verification error twice #2703)

• Dafny now compiles functions that mix tail- and non-tail-recursive calls without crashing (Crash during compilation in any language #2726)

• substitution of binding guards does not crash if splits present (Incorrect handling of split quantifier expressions in substitution of binding guards #2748)

• No more crash when constraining type synonyms (Dafny crash on a recursive definition #2829)

• Returning a tuple when it should be two variables does not crash Dafny anymore (ArgumentNullException in resolver (ProgramTraverser.Traverse) #2878)

• Default generic values no longer cause compilation error (Cannot compile default generic values in C# #2885)

• Now publishing Dafny Binary for MacOS Arm64 architecture (Update release process to include building a Dafny that's usable on M* Macs. #2889)

• Added a missing case in the Translator (pattern matching for variable declarations) (cce+UnreachableException in Microsoft.Dafny.Substituter.SubstStmt #2920)

• The Python and Go backends now encode non-ASCII characters in string literals correctly (fix: Handle UTF-16 escapes and invalid surrogate sequences in Python and Go #2926)

• Added a missing case of TypeSynonymDecl in the resolver that caused a crash (Crash on constrained subset of sequence type with explicit witness #2927)

• Fix malformed Boogie generated for extreme predicates (fix: Fill in missing type substitutions #2984)

• Counter-examples with non-integer sequence indices do not crash Dafny anymore. ([Bug]: Non-integer Seq#Indexes lead to LSP crash #3048)

• Use correct type for map update expression ([Bug]: subset type for maps fails to verify overriden key/value pairs #3059)

• Language server no longer crashing in special case (Crash of Language Server #3062)

• Resolved an instance in which the Dafny language server could enter a broken state. (Remove one instance of static state in the compilation pipeline #3065)

• Do not refer to an implicit assignment in error messages on return statements (Error messages on return statements may refer to an implicit assignment #3125)

• Multiple exact same failing assertions do not crash the Boogie counter-example engine anymore (Bumped boogie version to 2.16.0 #3136)

• Duplicate declarations caused by resolver do not crash the language server anymore (Another "item with the same key has already been added" instance #3155)

---

This discussion was created from the release Dafny 3.10.0.