Dafny 4.4.0

[robin-aws]

New features

• Reads clauses on method declarations are now supported when the --reads-clauses-on-methods option is provided.
  The {:concurrent} attribute now verifies that the reads and modifies clauses are empty instead of generating an auditor warning.
  (feat: Read clauses on methods #4440)

• Added two new options, --warn-contradictory-assumptions and --warn-redundant-assumptions, to detect potential problems with specifications that indicate that successful verification may be misleading. These options are currently hidden because they may occasionally produce false positives in cases where proofs are so trivial that the solver never does work on them. (Proof dependency warnings #4542)

• Verification of the {:concurrent} attribute on methods now allows non-empty reads and modifies clauses with the {:assume_concurrent} attribute. (feat: {:assume_concurrent} attribute #4563)

• Implemented support for workspace/symbol request to allow IDE navigation by symbol. (Provide workspace symbols from Dafny LSP #4619)

• The new --verification-coverage-report flag to dafny verify creates an HTML report highlighting which portions of the program were and were not necessary for verification. The format is the same as for dafny generate-tests --coverage-report and files from the two commands can be merged. (Verification coverage report #4625)

• Built-in types such as the nat subset type, tuples, arrows, and arrays are now pre-compiled into each backend's runtime library,
  instead of emitted on every call to dafny translate, to avoid potential duplicate definitions when translating components separately.
  (feat: Populate runtimes with all built-in declarations #4658)

• The new --only-label option to merge-coverage-reports includes only one category of highlighting in the output. For example, merging coverage reports from test generation and verification using the option --only-label NotCovered will highlight only the regions not covered by either testing or verification. (Allow filtering of combined coverage reports #4673)

• The Dafny distribution now includes standard libraries, available with the --standard-libraries option.
  See https://github.com/dafny-lang/dafny/blob/master/Source/DafnyStandardLibraries/README.md for details.
  (feat: Standard library support + DafnyStdLibs.Wrappers #4678)

• Introduce replaceable modules, which can be used to help define Dafny applications that translate to multiple target languages. (Add replaceable modules #4681)

• The new --coverage-report flag to dafny run and dafny test creates an HTML report highlighting which portions of the program were executed at runtime. (feat: Execution branch coverage report #4755)

• Enable turning nonlinear arithmetic on or off on a per-module basis, using the attribute {:disable-nonlinear-arithmetic},
  which optionally takes the value false to enable nonlinear arithmetic.
  (Allow disable-non-linear-arithmetic per module #4773)

• Let the IDE provide code navigation in situations where the program parses but has resolution errors. Note that this only works for modules whose dependency tree does not have errors, or modules who contain errors themselves, but not for modules whose dependencies contain errors. (Code navigation when resolution errors #4855)

Bug fixes

• Ensures that computing the set of values or items of map can only be done if the type of the range supports equality. (Verification: map should not allow .Values if the value type is not equality supporting #1373)

• Subset type decl's witness correctly taken into account (Crash during translation #3792)

• Added a comprehensive test for test generation and fixed a bug that prevented test generation to process function-by-method declarations ([Test Generation] Comprehensive Test #4406)

• Optimized memory consumption of test generation by reusing the Boogie AST of the target Dafny program. ([Test Generation] Reduce memory footprint by reusing the same Boogie program for multiple test generation queries #4530)

• Fix a bug that prevented certain types of lemma to be verified in the IDE (Fix least lemma IDE verification bug and add test #4607)

• Dot completion now works on values the type of which is a type synonym. ([LSP] Return completion options for type synonyms #4635)

• Fix a case where the document symbol API would return incorrect data when working on a file with parse errors (Do not let documentSymbol API return a faulty line  #4675)

• Emit less nested target code in match-case expressions (nice for readability, and necessary for Java) (Emit less nested target code #4683)

• Ghost diagnostics are now correctly updated when they become empty (Ghost diagnostics not correctly updated #4693)

• Enable verification options that are configured in a Dafny project file, to be picked up by the Dafny language server (Language server does not seem to respect options in project file #4703)

• Prevent double-counting of covered/uncovered lines in test coverage reports (Fix double counting of lines in test coverage reports #4710)

• fix: correction of type inference for default expressions (Crash using subset type #4724)

• The new type checker now also supports static reveals for instance functions (Allow static reveal of instance function in new resolver #4733)

• Resolve :- expressions with void outcomes in new resolver (fix: Resolve :- expressions with void outcomes in new resolver #4734)

• Crash in the resolver on type parameters of opaque functions in refined modules (Abstract module + type parameter crashes Dafny #4768)

• Fix error messages being printed after their context snippets (Redundant- and contradictory-assumptions warnings are incorrectly formatted #4787)

• Override checks no longer crashing when substituting type parameters and equality (Error proving override check #4812)

• Removed one cause of need for restarting the IDE. (Dafny IDE needs restarting every 3-4 minutes #4833)

• The Python compiler emits reserved names for datatypes (fix: The Python compiler emits reserved names for datatypes #4843)

---

This discussion was created from the release Dafny 4.4.0.