Dafny 1.9.4

Rating: No reviews yet
Downloads: 205
Change Set: 28b505580d47
Released: Apr 29, 2015
Updated: Apr 29, 2015 by rustanleino
Dev status: Stable Help Icon

Recommended Download

Application Dafny.zip
application, 9352K, uploaded Apr 29, 2015 - 205 downloads

Release Notes

Here are the major changes from version 1.9.1 to version 1.9.4:
  • Semi-colons are no longer needed at the end of specification clauses (like `requires`, `invariant`). Semi-colons are now required only as statement terminators, as terminators of lines in `calc` statements, in let expressions, and in statement expressions.
  • Names are now resolved in a different order, from local out to the module scope.
  • Type arguments can be user specified (using angle brackets after the name of the function or method).
  • Functions and methods declared at the module level are now automatically declared as static. In fact, the `static` keyword is no longer allowed to be placed on such functions and methods. With this change, fields are no longer allowed to be declared at the module level. (The `/allowGlobals` command-line switch can help with the transition from old code to new code where such fields are to be declared inside user-declared classes.)
  • Previously, functions were opaque outside the declaring module. That is, the body of a function was hidden from outside the module. This is no longer the case. To make a function opaque (both inside and outside the declaring module), use the `:opaque` attribute. The body can then be revealed using the corresponding `reveal_` lemma. To prevent the body from ever being revealed outside the declaring module, use the new `protected` modifier on the function.
  • A class can now extend multiple traits.
  • In addition to the finite-map type `map<T,U>`, there is now also a map type whose domain can be infinite: `imap<T,U>`.
  • A `newtype` that can fit into a native integral type now gets compiled into the smallest such type. This behavior can be customized by the `:nativeType` attribute.
  • Let-such-that expressions (aka Hilbert's epsilon operator) are now allowed in non-ghost code, provided they prescribe a unique value (as is checked by the verifier). (This restriction means that compiled let-such-that expressions really correspond to Hilbert's iota operator.)
  • Improvements in the fine-grained caching in the Dafny IDE. This caching is now turned on by default.
  • As the Dafny IDE starts up, it will read command-line options from a new file called `DafnyOptions.txt` in the .vsix plug-in directory.
  • The old vim mode for Dafny has been replaced by the vim-loves-dafny package.
  • `:trigger` attributes can now be used also in let and let-such-that expressions, in set, map, and imap comprehensions, and in assign-such-that statements.
  • Attribute `:timeLimitMultiplier` can be used as an alternative to `:timeLimit`. It computes a time limit as the product of the `/timeLimit` on the command line and the given multiplier.
  • Many bug fixes

Program safely!

Reviews for this release

No reviews yet for this release.