dafny-lang/dafny v1.9.7

Dafny 1.9.7

on GitHub

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

Language:

• New syntax for datatype update: D.(f := E) (instead of the previous D[f := E])
• New syntax: the previous import A as B is now import A : B
• Modules can now declare export views and these can be specified in imports
• Allow tuple-based assignment in statement contexts
• Syntactically computed bounds for quantified variables no longer depend on the order of the variables
  case can now use nullary tuple constructor

Verification:

• Changes in fuel handling
• Inline top-level predicates in method and iterator specifications
• The version of the included Z3 is 4.4.1
• Improved handling of arrow types and function values
• Enhancements in auto-triggers in forall statements
• Enhancement of {:autocontracts}
• Various bug fixes

Visual Studio IDE:

• /autoTriggers:1 is default in Visual Studio IDE (soon to become the default also in the Emacs IDE and from the command line)
• Cached results now depend on if a function is ghost or not
• Menu item in Visual Studio IDE to turn on/off automatic induction
• Fixed placement of blue dots in Visual Studio IDE
• Less duplication of hover text
• Fewer auto-generated variables shown in Verification Debugger

Compiler:

• Declarations can be declared extern to get a user-specified name in target code
• More liberal rules for selection of Main method, provided it is marked with {:main}
• Various bug fixes

Miscellaneous:

• Various bug fixes