dafny-lang/dafny v4.8.0

Dafny 4.8.0

on GitHub

New features

• Introduce hide statements that enable hiding the body of a function at a particular proof location, which allows simplifying the verification of that proof in case the body of the function is not needed for the proof. Hide statements make the opaque keyword on functions obsolete. Requires --type-system-refresh (#5562)

• Let the command measure-complexity output which verification tasks performed the worst in terms of resource count. Output looks like:

  Verification task on line 8 in file measure-complexity.dfy consumed 9984 resources
  Verification task on line 7 in file measure-complexity.dfy consumed 9065 resources
  

  (#5631)

• Enable the option --enforce-determinism for the commands resolve and verify (#5632)

• Method calls get an optional by-proof that hides the precondtion and its proof (#5662)

Bug fixes

• Clarify error location of inlined is predicates. (#5587)

• Optimize the compilation of single-LHS assignment statements to allow the RHS to be a deeply nested expression. This solves a problem in compiling to Java, since javac does not deal gracefully with nested lambda expressions. (#5589)

• Crash when compiling an empty source file while including testing code (#5638)

• Let the options --print-mode=NoGhostOrIncludes and --print-mode=NoIncludes work (#5645)

• Verification in the IDE now works correctly when declaring nested module in a different file than their parent. (#5650)

• Fix NRE that would occur when using --legacy-data-constructors (#5655)