Dafny 1.9.7

Rating: No reviews yet
Downloads: 1153
Change Set: 915d3365ca66
Released: Apr 1, 2016
Updated: Apr 2, 2016 by rustanleino
Dev status: Stable Help Icon

Recommended Download

Application Dafny 1.9.7 for Windows
application, 18433K, uploaded Apr 1, 2016 - 879 downloads

Other Available Downloads

Application Dafny 1.9.7 for Mac OSX
application, 31957K, uploaded Apr 2, 2016 - 83 downloads
Application Dafny 1.9.7 for Debian
application, 37178K, uploaded Apr 2, 2016 - 36 downloads
Application Dafny 1.9.7 for Ubuntu
application, 36293K, uploaded Apr 2, 2016 - 133 downloads
Application Dafny 1.9.7 for Free BSD
application, 33865K, uploaded Apr 2, 2016 - 22 downloads

Release Notes

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

Reviews for this release

No reviews yet for this release.