Skip to content

Dafny 1.9.8

Choose a tag to compare

View all tags
@RustanLeino RustanLeino released this 31 Aug 17:52
· 4683 commits to master since this release
v1.9.8
6df6129

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
Assets 7
Loading