You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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 (Hide statements #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
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. (Optimize compilation of functional-looking assignment RHSs #5589)
reacted with thumbs up emoji reacted with thumbs down emoji reacted with laugh emoji reacted with hooray emoji reacted with confused emoji reacted with heart emoji reacted with rocket emoji reacted with eyes emoji
-
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
(Hide statements #5562)Let the command
measure-complexity
output which verification tasks performed the worst in terms of resource count. Output looks like:(Let
measure-complexity
output the worst performing verification tasks by resource count #5631)Enable the option
--enforce-determinism
for the commandsresolve
andverify
(Enable the option enforce determinism for the verify command #5632)Method calls get an optional by-proof that hides the precondtion and its proof (feat: Method calls with a by-proof #5662)
Bug fixes
Clarify error location of inlined
is
predicates. (fix: Clarify error location of inlinedis
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. (Optimize compilation of functional-looking assignment RHSs #5589)Crash when compiling an empty source file while including testing code (fix: Crash when compiling an empty source file while including testing code #5638)
Let the options
--print-mode=NoGhostOrIncludes
and--print-mode=NoIncludes
work (Use a DafnyProject instead of a root file for printing #5645)Verification in the IDE now works correctly when declaring nested module in a different file than their parent. (parent modules break verification when included through project files #5650)
Fix NRE that would occur when using --legacy-data-constructors (Fix NRE and add test #5655)
This discussion was created from the release Dafny 4.8.0.
Beta Was this translation helpful? Give feedback.
All reactions