chore(deps): bump org.dafny:DafnyRuntime from 4.0.0 to 4.1.0 in /TestVectors/runtimes/java

[dependabot]

Bumps org.dafny:DafnyRuntime from 4.0.0 to 4.1.0.

Release notes

Sourced from org.dafny:DafnyRuntime's releases.

Dafny 4.1.0

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. (dafny-lang/dafny#2907)

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

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

• Added option --no-verify for language server (dafny-lang/dafny#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 (dafny-lang/dafny#3756)

• Documentation of the syntax for docstrings added to the reference manual (dafny-lang/dafny#3773)

• Labelled assertions and requires in functions (dafny-lang/dafny#3804)

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

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

... (truncated)

Changelog

Sourced from org.dafny:DafnyRuntime's changelog.

4.1.0

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. (dafny-lang/dafny#2907)

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

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

• Added option --no-verify for language server (dafny-lang/dafny#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 (dafny-lang/dafny#3756)

• Documentation of the syntax for docstrings added to the reference manual (dafny-lang/dafny#3773)

• Labelled assertions and requires in functions (dafny-lang/dafny#3804)

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

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

... (truncated)

Commits

• 78a5a95 Release Dafny 4.1.0
• 4053f90 chore: Fix NuGet release downloads workflow (#3975)
• de87ccf fix: Test and CI (#3983)
• 26cfdee Revert "Remove IncludeToken as prep for caching parsing (#3858)" (#3981)
• 298fbcb Fix: Format for comprehension expressions (#3916)
• bd2d4ec fix: Select alternative default calc operator more carefully (#3963)
• e803796 Adding utility functions; tightening types (#3973)
• e48820a Add --solver-option flag and move others around (#3943)
• a478a64 fix: Block .doo files as input in legacy CLI (#3967)
• 5134059 Adding tests for attribute help and other help (#3964)
• Additional commits viewable in compare view

Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting @dependabot rebase.

---

Dependabot commands and options

You can trigger Dependabot actions by commenting on this PR:

• @dependabot rebase will rebase this PR
• @dependabot recreate will recreate this PR, overwriting any edits that have been made to it
• @dependabot merge will merge this PR after your CI passes on it
• @dependabot squash and merge will squash and merge this PR after your CI passes on it
• @dependabot cancel merge will cancel a previously requested merge and block automerging
• @dependabot reopen will reopen this PR if it is closed
• @dependabot close will close this PR and stop Dependabot recreating it. You can achieve the same result by closing it manually
• @dependabot ignore this major version will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself)
• @dependabot ignore this minor version will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself)
• @dependabot ignore this dependency will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself)