Dafny 4.10.0

[MikaelMayer]

New features

• Support for code actions in the language server to:

  • Insert failing implicit assertions in a "by" clause by preference.
  • Insert forall statement for any forall expressions that could not be proved
  • Insert calc statement for any equality that cannot be proved. (Feat code actions forall calc #6044)

• Besides --filter-position :<line>, also support --filter-position :<start>- <end>, --filter-position :<start>- and --filter-position :-<end> (Enable filtering on a range of assertions #6077)

• The options --iterations from the command measure-complexity, has been renamed to --mutations. The option --progress VerificationJob has been renamed to --progress Batch. (Tweak the --progress option and rename the --iterations option #6078)

Bug fixes

• By clauses for assign-such-that statements (:|), are now never ignored. (by-clause ignored for assign-such-that statements #6024)

• The code action for assertion no longer suggests asserting the same assertion. (Useless and distracting code action #6025)

• Fix a bug that caused a crash when translating by blocks (Allow translating by blocks #6050)

---

This discussion was created from the release Dafny 4.10.0.