Dafny 3.11.0

[keyboardDrummer]

New features

• Go to definition now works reliably across all Dafny language constructs and across files. (Resolve match before compile #2734)

• Improve performance of Go code by using native byte/char arrays (Use native byte/char arrays in Go #2818)

• Introduce the experimental measure-complexity command, whose output can be fed to the Dafny report generator. In a future update, we expect to merge the functionality of the report generator into this command. (Introduce measure-complexity command #3061)

• Integrate the Dafny auditor plugin as a built-in dafny audit command. (Initial C# port of auditor #3175)

• Add the --solver-path option to allow customizing the SMT solver used when using the new Dafny CLI user interface. (Add the --solver-path option #3184)

• Add the experimental --test-assumptions option to all execution commands: run, build, translate and test.
  When turned on, inserts runtime tests at locations where (implicit) assumptions occur, such as when calling or being called by external code and when using assume statements.
  Functionality is still being expanded. Currently only checks contracts on every call to a function or method marked with the {:extern} attribute.
  (Add --test-assumptions option #3185)

• For the command translate, renamed the option --target into language and turned it into a mandatory argument. (Let target be an argument instead of an option for translate #3239)

• Havoc assignments now count as assignments for definite-assignment checks. Unless --enforce-determinism is used, no errors are given for arrays that are allocated without being initialized.
  (Def assignment update #3311)

• Enable passing a percentage value to the --cores option, which will use a percentage of the total number of logical cores on the machine for verification. (Relative load option in new CLI #3328)

Bug fixes

• Nonexistent files passed on the CLI result in a graceful exit (Passing a DLL path that doesn't exist raises an exception #2719)

• Check loop invariants on entry, even when such are the only proof obligations in a method. (fix: Count proof obligations of loop headers #3244)

• The :options attribute now accepts new style options --function-syntax and --quantifier-syntax (Enable new style options in the :options attribute #3252)

• Improved error messages for dafny translate (Validate language argument of translate command #3274)

• The :test attribute is now compatible with dafny run and dafny build (Allow the :test attribute when using run and build #3275)

• Settings --cores=0 will cause Dafny to use half of the available cores. (Setting cores to 0 will use half of the available cores #3276)

• Remove an infeasible assertion in the Dafny Runtime for Java (fix: Remove infeasible assertions in the Dafny Runtime for Java #3280)

• Language server displays more relevant informations on hovering assertions (More relevant information on hovering failing assertions #3281)

• Any (==) inferred for a type parameter of an iterator is now also inferred for the corresponding non-null iterator type. (refactor: Clean up resolution passes 0 and 1 #3284)

• the otherwise ambiguous program fragment export least predicate is parsed such that least (or greatest) is the export identifier (Resolve ambiguity in export least predicate #3291)

• The parser generated bad tokens when invoked through /library (fix: Add substitute Include for /library #3301)

• dafny build for Java now creates a library or executable jar file.

  • If there is a Main method, the jar is an executable jar. So a simple A.dfy can be built as dafny build -t:java A.dfy
    and then run as java -jar A.jar
  • If there is no Main entry point, all the generated class files are assembled into a library jar file that can be used on a
    classpath as a java library.
  • In both cases, the DafnyRuntime library is included in the generated jar.
  • In old and new CLIs, the default location and name of the jar file is the name of the first dfy file, with the extension changed
  • In old and new CLIs, the path and name of the output jar file can be given by the --output option, with .jar added if necessary
  • As before, the compilation artifacts (.java and .class files) are placed in a directory whose name is the same as the jar file
    but without the .jar extension and with '-java' appended
  • With the new CLI, the generated .java artifacts are deleted unless --spill-translation=true and the .class files are deleted in any case;
    both kinds of files are retained with the legacy CLI for backwards compatibility.
  • If any other jar files are needed to compile the dafny/java program, they must be on the CLASSPATH;
    the same CLASSPATH used to compile the program is needed to run the program

  Having a library or executable jar simplifies the user's task in figuring out how to use the built artifacts.
  (Jar files, both library and executable, are now created as part of build on Java #3355)

• Proper warning that 'new' cannot be used in expressions, instead of a parse error (Parse failure on Some(new C<nat>(0)) #3366)

• The attributes :dllimport and :handle are now deprecated. They were undocumented, untested, and not maintained. (Deprecate :dllimport and :handle #3399)

• Fixed an axiom related to sequence comprehension extraction (Higher-order functions problem #3411)

---

This discussion was created from the release Dafny 3.11.0.