Dafny 4.9.0

[MikaelMayer]

New features

• Added opaque blocks to the language. Opaque blocks enable improving verification performance. See the documentation for more details. (Opaque block #5761)

• By blocks (... by { ... }) are now available for assert statements, call statements, and the three types of assignments (:=, :-, :|). Also, by blocks should now be more intuitive since they enable proving any assertions on the left-hand side of the 'by', not just the 'outermost' one. For example, previously assert 3 / x == 1 by { assume x == 3; } used to give a possible division by zero error, but now it won't. (Penetrating by blocks #5779)

• Use --suggest-proof-refactoring to be alerted of function definitions, which have no contribution to a method's proof, and facts, which are only used once in a proof. (feat: Proof refactoring suggestions #5812)

• Support for top-level @-attributes (Feat: @-attributes on top-level declarations #5825)

Bug fixes

• Enable abstract imports to work well with match expression that occur in specifications (Internal error during verification #5808)

• Fix a bug that prevented using reveal statement expressions in the body of a constant. (Add test and fix bug for use of reveal within a constant #5823)

• Improve performance of dafny verify for large applications, by removing memory leaks (Speed up dafny verify by reducing memory pressure #5827)

• Green gutter icons cover constants without RHS (Gutter icons broken for constant without RHS #5841)

---

This discussion was created from the release Dafny 4.9.0.