New features
-
Added opaque blocks to the language. Opaque blocks enable improving verification performance. See the documentation for more details. (#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, previouslyassert 3 / x == 1 by { assume x == 3; }used to give a possible division by zero error, but now it won't. (#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. (#5812)
-
Support for top-level @-attributes (#5825)
Bug fixes
-
Enable abstract imports to work well with match expression that occur in specifications (#5808)
-
Fix a bug that prevented using reveal statement expressions in the body of a constant. (#5823)
-
Improve performance of
dafny verifyfor large applications, by removing memory leaks (#5827) -
Green gutter icons cover constants without RHS (#5841)