dafny-lang/dafny v4.11.0

Dafny 4.11.0

on GitHub

New features

• Stabilize verifications by automatically computing triggers for the quantified proof obligations associated with :| constructs.
  Manually specified triggers and warning-suppressing attributes are also supported (and mentioned in warning messages, as for other quantifiers and comprehensions).
  Enhance witness guessing for the proof obligation associated for :| assignments.
  (#6023)

• Four new Dafny standard libraries:

  • Std.Actions - utilities for abstract imperative actions, including enumerating and streaming values
  • Std.Frames - utilities related to working with dynamic framing, often related to reads and modifies clauses
  • Std.Ordinal - operations and properties of the ORDINAL type
  • Std.Termination - a datatype for representing Dafny decreases clauses and extensions
    (#6074)

• Support using --standard-libraries with --enforce-determinism. Removed Std.Collections.Seq.SetToSeq since it was slow and not compatible with this mode. (https://github.com/dafny-lang/daf
  ny/pull/6137)

• With --standard-libraries you can now read an UTF-8 text files from the disk using Std.FileIO.ReadUTF8FromFile(path: string): Result<string, string>.
  To write some content to the disk, use Std.FileIO.WriteUTF8ToFile(path: string, content: string): Outcome<string>.
  Standard library breaking change: All UnicodeEncodingForm versions of FromUTF8Checked, FromUTF16Checked and DecodeCodeUnitSequenceChecked now return a Result instead of an Option so that the error message is clearer. Migration is easy: Use .ToOption() if you really prefer an option. Affected refining modules: Utf8EncodingForm and Utf16EncodingForm
  (#6198)

• The Dafny standard libraries now include a powerful parser combinators framework, available through Std.Parsers.StringBuilders.

  Key Features

  • Guaranteed Termination: All parsers, including those built with recursive combinators, are proven to terminate
  • Mutual Recursion Support: Build complex parsers that can reference each other (demonstrated in the Polynomial example)
  • Rich Error Reporting: Failed parsing attempts combine their error messages to provide meaningful feedback
  • Developer-Friendly Tools: Built-in debugging utilities for inspecting parser inputs and outputs
  • Memory-Efficient Recursion: Advanced implementations avoid stack overflow in recursive parsers
  • Elegant DSL: Compact, datatype-based combinators designed for readability and composition
  • Flexible Backtracking: Optional backtracking available through .??() (DSL) or ?(...) (standard syntax)
  • Comprehensive Toolkit: Rich set of combinators including lookahead, negation, folding, and binding operations
  • The library includes several practical examples, including JSON and SMT parsers, each implemented in about 50 lines of code.
    (#6243)

• Dafny classes and traits can now redeclare methods defined by traits they inherit from. (#6280)

• Real literals now support scientific notation using lowercase e to denote the exponent (like 1.23e5 for 123000.0 or 5e-2 for 0.05). Real literals also support convenient trailing-dot
  shorthand (like 1. for 1.0) and leading-dot shorthand (like .5 for 0.5 or .5e2 for 50.0). Note that explicit + signs in exponents are not supported; use 5e2 instead of 5e+2. (ht
  tps://github.com//pull/6286)

Bug fixes

• Fix soundness issue that could occur when using an opaque block and old or fresh in its ensures clause (#6060)

• Correctly display project files errors when using build command (#6107)

• Fix crash that could occur when a forall statement was used inside a match case (#6121)

• Fix a case where a forall statement would cause Dafny to crash (#6129)

• Fix @VerifyOnly and migrated the new code to use it (#6146)

• Java lambdas now accepting boxing/unboxing (#6149)

• Fix crash in resolution of structural-inclusion greater-than operator (#6155)

• Generate alloc consequence axiom only for functions that read the heap (fixes unsoundness) (#6164)

• Made the language server compliant with the LSP protocol so that it can be used with other editors, such as Helix (#6172)

• No more compilation issue when using bitvector shifts in Rust with the new resolver (#6196)

• Fix handling of opaque blocks in the Dafny IDE (#6203)

• JSON serialization now properly encodes unicode characters with 0 pre-pend instead of space-append.
  Also, string literals ending with escaped characters are now supported as well.
  (#6227)

• Fail more gracefully when reusing names (#6262)

• Escape user string literals in error messages (#6273)

• Compilation of type conversion from a newtype-based on char to int (#6296)

• Fix LSP bug that cause IDE exceptions during invalid parse states (#6299)

• Fix two resolver crashes involving datatypes and traits (#6321)