Dafny 1.9.1

Rating: No reviews yet
Downloads: 1057
Change Set: 76ef5c01b350
Released: Oct 22, 2014
Updated: Oct 22, 2014 by rustanleino
Dev status: Stable Help Icon

Recommended Download

Application Dafny.zip
application, 3930K, uploaded Oct 22, 2014 - 1057 downloads

Release Notes

Dafny version 1.9.1 includes some major changes over version 1.8.2,

Language changes that break backward compatibility:
  • Declarations and invocations of nullary predicates now require parentheses (to distinguish invocations from using the predicate as a first-class function value)
  • Stricter rules for ambiguously specified types (may require additional manually supplied types, since type inference may now in some cases do less)
  • Function "reads" clauses now need to frame themselves and preconditions
  • Changed behavior of "decreases * ". To use "decreases * ", the enclosing context must also allow "decreases * ". (Consequently, note that "decreases * " is now allowed on any method, not just on tail recursive methods, which increases the chance that non-terminating methods may run out of stack space.) Also, "decreases * " is now inherited in refining modules.
  • Type conversion from "real" to "int" no longer does truncation, but instead is defined only if the "real" has no fractional part. To truncate a "real", use the new ".Trunc" member.
  • Identifier names are no longer allowed to contain backslashes

New language features:
  • First-class functions (higher-order functions), lambda expressions
  • "newtype" declaration for user-defined numeric types
  • Built-in tuple types and tuples
  • Traits (abstract superclasses), basic features
  • Types "char" and "string" (this is the difference between version 1.9.0 and version 1.9.1)
  • User-defined type synonyms
  • Opaque types can now take type parameters
  • Syntax for "match" expressions and "match" statements the same --- curly braces around the cases are now supported for both and are optional for both
  • Change in scoping to allow a datatype to have a constructor with the same name.
  • Auto-declaration of type parameters used in signatures
  • Type parameters for arrays and collection types can now be filled in automatically in signatures
  • Datatype rank comparison, written "<", now allows type of left operand to be a type parameter
  • reads clauses now accept arguments of type "A -> set<object>"

Improvements in verification:
  • Computations can now also include sequences and lambda literals
  • Improved triggering in "forall" assignment statements
  • Command-line support for verifying snapshots
  • New logical encoding of types, supporting type parameters properly

Dafny IDE enhancements:
  • Now works in both Visual Studio 2012 and Visual Studio 2013
  • Advanced caching of verification results
  • Compilation output is now display in the Visual Studio Output pane
  • Shorter wait-for-idle time

  • Various bug fixes

Reviews for this release

No reviews yet for this release.