Dafny 3.6.0

[cpitclaudel]

• feat: The synthesize attribute on methods with no body allows synthesizing objects based on method postconditions at compile time (currently only available for C#). See Section 22.2.20 of the Reference Manual. (Support for Mocking in C# Compiler #1809)
• feat: The /verificationLogger:text option now prints all verification results in a human-readable form, including a description of each assertion in the program.
• feat: The /randomSeedIterations:<n> option (from Boogie) now tries to prove each verification condition n times with a different random seed each time, to help efficiently and conveniently measure the stability of verification. (Add /randomSeedIterations flag for verification stability analysis boogie-org/boogie#567)
• feat: The new /runAllTests can be used to execute all methods with the {:test} attribute, without depending on a testing framework in the target language.
• feat: Recognize !in operator when looking for compilable comprehensions (Bounded pool for not in #1939)
• feat: The Dafny language server now returns expressions ranges instead of token ranges to better report errors (Feat: Added ranges to expression #1985)
• fix: Miscompilation due to incorrect parenthesization in C# output for casts. (fix(compiler): Add parentheses around C# casts to fix #1714 #1908)
• fix: Populate TestResult.ResourceCount in /verificationLogger:csv output correctly when verification condition splitting occurs (e.g. when using /vcsSplitOnEveryAssert).
• fix: DafnyOptions.Compiler was null, preventing instantiation of ModuleExportDecl (fix: DafnyOptions.O.Compiler is null, preventing instantiation of ModuleExportDecl #1933)
• fix: /showSnippets crashes Dafny's legacy server (fix: Disable /showSnippets in legacy Dafny server (fixes #1969) #1970)
• fix: Don't check for name collisions in modules that are not compiled (fix: Don't check CompileName of modules with {:compile false} (fixes #1966) #1998)
• fix: Allow datatype update expressions for constructors with nameonly parameters (fix: Allow datatype update expressions for constructors with nameonly parameters #1949)
• fix: Fix malformed Java code generated for comprehensions that use maps (Bounded pool for not in #1939)
• fix: Comprehensions with nested subset types fully supported, subtype is correctly checked (Fix: Emit constraints for compiled quantifier expressions, and nested subset types #1997)
• fix: Fix induction hypothesis generated for lemmas with a receiver parameter (fix: Substitute for receiver in automatically generated induction hypothesis #2002)
• fix: Make verifier understand (!new) (fix: Make verifier understand (!new) #1935)
• feat: Some command-line options can now be applied to individual modules, using the {:options} attribute. (feat: Add an :options attribute on modules #2073)
• fix: Missing subset type check in datatype updates (fix: Use correct type for let expression generated by datatype update #2059)
• fix: Fix initialization of non-auto-init in-parameters in C#/JavaScript/Go compilers (fix: Make verifier understand (!new) #1935)
• fix: Resolution of static functions-by-method (fix: Resolution of static functions-by-method #2023)
• fix: Export sets did not work with inner modules (fix: Clone entire LiteralModuleDecl #2025)
• fix: Prevent refinements from changing datatype and newtype definitions (Sequence implementation in Go missing Elements() method #2038)
• feat: The new older modifier on arguments to predicates indicates that a predicate ensures the allocatedness of some of its arguments. This allows more functions to show that their quantifiers do not depend on the allocation state. For more information, see the reference manual section on older. (feat: Introduce :older attribute #1936)
• fix: Fix (!new) checks (function value can depend on set of allocated objects #1419)
• fix: multiset keyword no longer crashes the parser (fix: calc of multiset crashes #2079)

---

This discussion was created from the release Dafny 3.6.0.