Dafny Versions Save

Dafny is a verification-aware programming language

v4.6.0

1 month ago

New features

Bug fixes

v4.5.0

2 months ago

New features

  • Add the option --include-test-runner to dafny translate, to enable getting the same result as dafny test when doing manual compilation. (https://github.com/dafny-lang/dafny/pull/3818)

    • Fix: verification in the IDE no longer fails for iterators
    • Fix: the IDE now provides feedback when verification fails to run, for example due to a bad solver path
    • Fix: let the IDE correctly use the solver-path option when it's specified in a project file
    • Feat: improve the order of verification diagnostics emitted by the Dafny CLI, so that they now always follow the line order of the program. (https://github.com/dafny-lang/dafny/pull/4798)
    • Add an option --filter-position to the dafny verify command. The option filters what gets verified based on a source location. The location is specified as a file path suffix, optionally followed by a colon and a line number. For example, dafny verify dfyconfig.toml --filter-position=source1.dfy:5 will only verify things that range over line 5 in the file source1.dfy. In combination with ``--isolate-assertions, individual assertions can be verified by filtering on the line that contains them. When processing a single file, the filename can be skipped, for example: dafny verify MyFile.dfy --filter-position=:23`
    • Add an option --filter-symbol to the dafny verify command, that only verifies symbols whose fully qualified name contains the given argument. For example, dafny verify dfyconfig.toml --filter-symbol=MyModule will verify everything inside MyModule.
    • The option --boogie-filter has been removed in favor of --filter-symbol (https://github.com/dafny-lang/dafny/pull/4816)

  • Add a json format to those supported by --log-format and /verificationLogger, for producing thorough, machine readable logs of verification results. (https://github.com/dafny-lang/dafny/pull/4951)

    • Flip the behavior of --warn-deprecation and change the name to --allow-deprecation, so the default is now false, which is standard for boolean options.
    • When using --allow-deprecation, deprecated code is shown using tooltips in the IDE, and on the CLI when using --show-tooltips.
    • Replace the option --warn-as-error with the option --allow-warnings. The new option, when false, the default value, causes Dafny to stop generating executable output and return a failure exit code, when warnings occur in the program. Contrary to the previous --warn-as-error option, warnings are always reported as warnings.
      • During development, users must use dafny run --allow-warnings if they want to run their Dafny code when it contains warnings.
      • If users have builds that were passing with warnings, they have to add --allow-warnings to allow them to still pass.
      • If users upgrade to a new Dafny version, and are not using --allow-warnings, and do not want to migrate off of deprecated features, they will have to use --allow-deprecation.
    • When using the legacy CLI, the option /warningsAsErrors now has the behavior of --allow-warnings=false
    • A doo file that was created using --allow-warnings causes a warning if used by a consumer that does not use it. (https://github.com/dafny-lang/dafny/pull/4971)

  • The new {:contradiction} attribute can be placed on an assert statement to indicate that it forms part of an intentional proof by contradiction and therefore shouldn't be warned about when --warn-contradictory-assumptions is turned on. (https://github.com/dafny-lang/dafny/pull/5001)

  • Function and method parameters and return types, and datatype constructor arguments, can now have attributes. By default, there are no attributes that Dafny recognizes in these positions, but custom back-ends can use this feature to get extra information from the source files. (https://github.com/dafny-lang/dafny/pull/5032)

  • Under the CLI option --general-newtypes, the base type of a newtype declaration can now be (int or real, as before, or) bool, char, or a bitvector type.

    as and is expressions now support more types than before. In addition, run-time type tests are supported for is expressions, provided type parameters are injective (as was already required) and provided the constraints of any subset type or newtype is compilable. Note, although both as and is allow many more useful cases than before, using --general-newtypes will also forbid some unusual cases that were previously allowed. Any such case that is now forbidden can still be done by doing the as/is via int. (https://github.com/dafny-lang/dafny/pull/5061)

  • Allow newtype declarations to be based on set/iset/multiset/seq. (https://github.com/dafny-lang/dafny/pull/5133)

Bug fixes

v4.4.0

5 months ago

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. (https://github.com/dafny-lang/dafny/pull/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. (https://github.com/dafny-lang/dafny/pull/4542)

  • Verification of the {:concurrent} attribute on methods now allows non-empty reads and modifies clauses with the {:assume_concurrent} attribute. (https://github.com/dafny-lang/dafny/pull/4563)

  • Implemented support for workspace/symbol request to allow IDE navigation by symbol. (https://github.com/dafny-lang/dafny/pull/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. (https://github.com/dafny-lang/dafny/pull/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. (https://github.com/dafny-lang/dafny/pull/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. (https://github.com/dafny-lang/dafny/pull/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. (https://github.com/dafny-lang/dafny/pull/4678)

  • Introduce replaceable modules, which can be used to help define Dafny applications that translate to multiple target languages. (https://github.com/dafny-lang/dafny/pull/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. (https://github.com/dafny-lang/dafny/pull/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. (https://github.com/dafny-lang/dafny/pull/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. (https://github.com/dafny-lang/dafny/pull/4855)

Bug fixes

v4.3.0

7 months ago

New features

  • Add support for the Find References LSP request

  • Improve scalability of inlining for test generation and generate coverage information with respect to the original Dafny source (https://github.com/dafny-lang/dafny/pull/4255)

  • Support generating of tests targeting path-coverage of the entire program and tests targeting call-graph-sensitive block coverage (referred to as Branch coverage) (https://github.com/dafny-lang/dafny/pull/4326)

  • Add support for Rename LSP request

  • Make verification in the IDE more responsive by starting verification after translating the required module to Boogie, instead of first translating all modules that could be verified. (https://github.com/dafny-lang/dafny/pull/4378)

  • The Dafny IDE now has improved behavior when working with a Dafny file that's part of a Dafny project. A Dafny file is part of a project if a dfyconfig.toml can be found somewhere in the file's path hierarchy, such as in the same folder or in the parent folder. A dfyconfig.toml can specify which Dafny options to use for that project, and can specify which Dafny files are part of the project. By default, the project will include all .dfy files reachable from the folder in which the dfyconfig.toml resides. Project related features of the IDE are:

    • Whenever one file in the project is opened, diagnostics for all files in the Dafny project are shown. When including a file with errors that's part of the same project, the message "the included file contains errors" is no longer shown. Instead, the included file's errors are shown directly.
    • If any file in the project is changed, diagnostics for all files in the project are updated. Without a project, changing an included file will not update diagnostics for the including file until the including file is also changed.
    • The find references feature (also added in this release), works better in files that are part of a project, since only then can it find references that are inside files that include the current file.
    • The assisted rename feature (also added in this release), only works for files that are part of a project.
    • When using a project file, it is no longer necessary to use include directives. In the previous version of Dafny, it was already the case that the Dafny CLI, when passed a Dafny project file, does not require include directives to process the Dafny program. The same now holds for the Dafny IDE when working with Dafny files for which a project file can be found.
    • If any file in the project is resolved, all files in the project are resolved. Opening a file in a project that's already resolved means the opened file is resolved instantly.
    • The IDE's memory consumption stays the same regardless of how many files in a project are opened. Without a project, the IDE increases it's memory usage for each open file.

    Try out the IDE's project support now by creating an empty dfyconfig.toml file in the root of your project repository. (https://github.com/dafny-lang/dafny/pull/4435)

  • Prior to generating tests, Dafny now checks the targeted program for any features that test generation does not support or any misuse of test generation specific attributes. Any such issues are reported to the user. (https://github.com/dafny-lang/dafny/pull/4444)

  • Added documentation of the generate-tests command to the reference manual (https://github.com/dafny-lang/dafny/pull/4445)

  • When two modules in the same scope have the same name, Dafny now reports an error that contains the location of both modules. (https://github.com/dafny-lang/dafny/pull/4499)

    • The Dafny IDE will now report errors that occur in project files.
    • The Dafny IDE will now shown a hint diagnostic at the top of Dafny project files, that says which files are referenced by the project. (https://github.com/dafny-lang/dafny/pull/4539)

Bug fixes

v4.2.0

9 months ago

New features

Bug fixes

v4.1.0

1 year ago

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. (https://github.com/dafny-lang/dafny/pull/2907)

  • Recognize the {:only} attribute on assert statements to temporarily transform other assertions into assumptions (https://github.com/dafny-lang/dafny/pull/3095)

  • Exposes the --output and --spill-translation options for the dafny test command (https://github.com/dafny-lang/dafny/pull/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. (https://github.com/dafny-lang/dafny/pull/3660)

  • Added option --no-verify for language server (https://github.com/dafny-lang/dafny/pull/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 (https://github.com/dafny-lang/dafny/pull/3756)

  • Documentation of the syntax for docstrings added to the reference manual (https://github.com/dafny-lang/dafny/pull/3773)

  • Labelled assertions and requires in functions (https://github.com/dafny-lang/dafny/pull/3804)

  • API support for obtaining the Dafny expression that is being checked by each assertion (https://github.com/dafny-lang/dafny/pull/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 .... (https://github.com/dafny-lang/dafny/pull/3913)

  • Semantic interpretation of dots in names for {:extern} modules when compiling to Python (https://github.com/dafny-lang/dafny/pull/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 (https://github.com/dafny-lang/dafny/pull/3940)

Bug fixes

v4.0.0

1 year ago

Breaking changes Remove deprecated countVerificationErrors option (https://github.com/dafny-lang/dafny/issues/3165)

The default version of Z3 Dafny uses for verification is now 4.12.1. (https://github.com/dafny-lang/dafny/pull/3400)

The default values of several options has changed in Dafny 4.0. See --help for details.

--function-syntax changed from 3 to 4 --quantifier-syntax changed from 3 to 4 --unicode-char changed from false to true (https://github.com/dafny-lang/dafny/pull/3623) The default value of the /allocated option is now 4, and the option itself is deprecated. (https://github.com/dafny-lang/dafny/pull/3637)

Compilation to Go no longer attempts to use the Dafny string type and the Go string type interchangably when calling external methods (which was buggy and unsound). (https://github.com/dafny-lang/dafny/pull/3647)

v3.13.1

1 year ago

Bug fixes

  • Restore publishing language server to nuget
  • Fix allow_on_mac.sh for z3 paths

v3.13.0

1 year ago

New features

Bug fixes

v3.12.0

1 year ago

New features

Bug fixes