dafny-lang/dafny v4.1.0

Dafny 4.1.0

on GitHub

New features

• Added support for .toml based Dafny project files. For now the project file only allows specifying which Dafny files to include and exclude, and what options to use.
  The CLI commands that take Dafny files as input, such as build, run, translate, will now also accept Dafny project files.
  When using an IDE based on dafny server, such as the Dafny VSCode extension, the IDE will look for a Dafny project file by traversing up the file tree from the currently opened file, until it finds it dfyconfig.toml. The project file will override options specified in the IDE.
  (#2907)

• Recognize the {:only} attribute on assert statements to temporarily transform other assertions into assumptions (#3095)

• Exposes the --output and --spill-translation options for the dafny test command (#3612)

• The dafny audit command now reports instances of the {:concurrent} attribute, intended to flag code that is intended, but can't be proven, to be safe for use in a concurrent setting. (#3660)

• Added option --no-verify for language server (#3732)

• Documenting Dafny Entities

  • Added .GetDocstring(DafnyOptions) to every AST node
  • Plugin support for custom Docstring formatter,
  • Activatable plugin to support a subset of Javadoc through --javadoclike-docstring-plugin
  • Support for displaying docstring in VSCode
    (#3756)

• Documentation of the syntax for docstrings added to the reference manual (#3773)

• Labelled assertions and requires in functions (#3804)

• API support for obtaining the Dafny expression that is being checked by each assertion (#3888)

• Added a "Dafny Library" backend, which produces self-contained, pre-verified .doo files ideal for distributing shared libraries.
  .doo files are produced with commands of the form dafny build -t:lib ....
  (#3913)

• Semantic interpretation of dots in names for {:extern} modules when compiling to Python (#3919)

• Code actions in editor to explicit failing assertions.
  In VSCode, place the cursor on a failing assertion that support being made explicit and either

  • Position the caret on a failing assertion, press CTRL+; and then ENTER
  • Hover over the failing division by zero, click "quick fix", press ENTER
    Both scenarios will explicit the failing assertion.
    If you don't see a quick fix, it means that the assertion cannot be automatically made explicit for now.

  Here is a initial list of assertions that can now be made explicit:

  • Division by zero
  • "out of bound" on sequences index, sequence slices, or array index
  • "Not in domain" on maps
  • "Could not prove unicity" of var x :| ... statement
  • "Could not prove existence" of var x :| ... statement
    (#3940)

Bug fixes

• dafny test accepts a --methods-to-test option whose value is a regular expression selecting which tests to include in the test run (#3221)

• The deprecated attributes :dllimport, :handle, and :heapQuantifier are no longer recognized. (#3398)

• While using dafny translate --target=java, the --include-runtime option works as intended, while before it had no affect. (#3611)

• Tested support for paths with spaces in them (#3683)

• Crash related to the override check for generic functions (#3692)

• Opaque functions guaranteed to be opaque until revealed (#3719)

• Support for Corretto tests (#3731)

• Right shift on native byte has the same consistent semantics even in Java (#3734)

• Main and {:test} methods may now be in the same program (#3744)

• The formatter now produces the same output whether invoked on the command-line or from VSCode (#3790)

• The --solver-log option is now hidden from help unless --help-internal is used. (#3798)

• Highlight "inconclusive" as errors in the gutter icons (#3821)

• Docstring for functions with ensures (#3840)

• Prevent a compiler crash that could occur when a datatype constructor was defined that has multiple parameters with the same name. (#3860)

• Improved rules for nameonly parameters and parameter default-value expressions (#3864)

• Fixes several compilation issues, mostly related to subset types defined by one of its type parameter (#3893)

• Explicitly define inequality of multisets in Python for better backwards compatibility (#3904)

• Format for comprehension expressions (#3912)

• Formatting for parameter default values (#3944)

• Formatting issue in forall statement range (#3960)

• Select alternative default calc operator only if it doesn't clash with given step operators (#3963)