dafny-lang/dafny v4.10.0

Dafny 4.10.0

on GitHub

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. (#6044)

• Besides --filter-position :<line>, also support --filter-position :<start>- <end>, --filter-position :<start>- and --filter-position :-<end> (#6077)

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

Bug fixes

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

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

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