dafny-lang/dafny v1.9.8

Dafny 1.9.8

on GitHub

Here are the major changes from version 1.9.7 to version 1.9.8:

Language:

• Binding if-then-else expressions (e.g., if x :| P(x) then S else T)
• New syntax for module export sets
• Added bitvector types and operations
• Added user-defined subset types and changed nat into a built-in subset type
• Added first-cut design of two-state lemmas
• Changed syntax of type coercions from int(x) to x as int, etc.
• Added assert ... by { ... } statement
• Braces around cases of alternative if/while statements now optional, just like for match statements
• Allow reads clauses of lambda expressions to take a comma-delimited list of frame expressions, not just one frame expression
• Renamed real.Trunc to the more appropriate name real.Floor
• Multiset of objects allowed in reads clauses
• Enforce that a function is allocated in the state in which it is invoked
• A warning is generated for body-less loops and forall statements
• Warning about shadowed variables can be suppressed with the :warnShadowing false attribute
• More elaborate :autocontracts

Type checking:

• Proper handling of subtypes
• Fixed resolution bugs related to modules

Verification:

• New design for :fuel annotations
• :opaque implemented in terms of :fuel
• Fixed a Mono warning in VerificationTask
• Improved translation of set comprehensions
• Fixed missing checks related to multi-dimensional arrays
• Improved encoding of let-such-that expressions
• Improved auto triggers, and make them the default
• Consequence axioms trigger off of any fuel
• Various other improvements and bug fixes

IDEs:

• Tooltips showing any inverter rewrites of forall-statements
• Italicize attributes and highlight recognized attributes in the VS IDE
• Improved syntax highlighting in VS IDE
• Goto definition (F12) in VS IDE
• F5 to toggle start/stop verifier and F11 to toggle start/stop resolver in VS IDE
• Improved pretty printing

Compiler:

• Command-line option /out:<file> to specify output filename for the generated .cs, .dll, or .exe files
• Added /deprecated flag to control which kinds of deprecation messages to bother the user with
• Embed Dafny source in compiled assembly
• Various bug fixes