Dafny 1.9.6

Rating: No reviews yet
Downloads: 1229
Change Set: 4d9578af5c7c
Released: Oct 12, 2015
Updated: Oct 12, 2015 by rustanleino
Dev status: Stable Help Icon

Recommended Download

Application Dafny 1.9.6 for Windows
application, 18493K, uploaded Oct 12, 2015 - 967 downloads

Other Available Downloads

Application Dafny 1.9.6 for Mac OSX
application, 32017K, uploaded Oct 12, 2015 - 104 downloads
Application Dafny 1.9.6 for Debian
application, 37238K, uploaded Oct 12, 2015 - 48 downloads
Application Dafny 1.9.6 for Ubuntu
application, 36353K, uploaded Oct 12, 2015 - 88 downloads
Application Dafny 1.9.6 for Free BSD
application, 33925K, uploaded Oct 12, 2015 - 22 downloads

Release Notes

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

Language changes:
  • Nested patterns in match statements and match expressions
  • Infinite sets and infinite maps (iset and imap) as built-in collection types
  • Reads checks of function preconditions and bodies are now postponed until after these have otherwise been checked for well-formedness. Also, reads clauses can now assume the precondition.
  • Binding guards to if statements
  • {:fuel … } attribute that allows a user to specify how many times the verifier is allowed to unfold a function’s definition. See changeset 8cce226a046c for details.
  • Type parameters in method/function signatures are no longer auto-declared. However, the functionality that fills in type parameters in signatures remains.
  • Command-line option /warnShadowing emits warnings if variables shadow other variables
  • Each “focal predicate” P is rewritten to P#[_k-1] in inductive/coinductive lemmas

  • Under command-line option /autoTriggers:1, Dafny selects matching triggers for user-defined quantifiers. This can significantly improve the verification experience. Warnings are produced for quantifiers with bad or no trigger choices, and the selected triggers can be inspected in hover texts.
  • Bug fixes and improvements for higher-order functions
  • Dafny now uses Z3 version 4.4
  • Improvements in the bounds discovery
  • Improved rank axioms for containers
  • Experimental support for diagnosing timeouts

  • /optimize flag for better-performing containers
  • newtype declarations of types that fit into native integer sizes are now compiled as such
  • Improved target code in compilation

IDEs and platforms:
  • Dafny server mode used by emacs mode for Dafny
  • Improved support for installing and running Dafny on Linux and Mac
  • Improved support for building Dafny under Linux with Mono
  • Tool tips (hover text) now shown also for the chosen induction variables
  • command-line option /printTooltips prints tool tips
  • consistent column numbers in output

  • Miscellaneous bug fixes

Reviews for this release

No reviews yet for this release.