Dafny 1.8.0

Rating: No reviews yet
Downloads: 131
Change Set: 56a6211f84dc
Released: Jan 15, 2014
Updated: Jan 16, 2014 by rustanleino
Dev status: Stable Help Icon

Recommended Download

Application Dafny.zip
application, 3315K, uploaded Jan 16, 2014 - 131 downloads

Release Notes

Here are some new things since version 1.7:
  • new "include" construct makes it easier to work with programs that are split into multiple files
  • "match" expressions can now be used in general positions (and axioms generated for functions defined by "match" expressions are now no different than other function axioms)
  • left-hand sides of let expressions can now be (possibly nested) patterns
  • a function F can be marked with {:opaque} to say that its body will not be visible; in places where the defining body is desired, call the pre-defined lemma reveal_F()
  • added more hover text in Dafny IDE (in Visual Studio), for example for inferred tool-provided clauses
  • changed location of the "blue dots" that show execution-trace information in the Dafny IDE
  • variables introduced by let expressions can now be declared ghost
  • a new {:axiom} attribute suppresses compiler warnings about missing bodies
  • compiler now always generates code for assign-such-that expression where the target variables are of type integer
  • new option /compiler:3 compiles and then runs the program
  • new {:autoReq} attribute constructs function preconditions from the preconditions of other functions called
  • command-line option /verifySeparately treats multiple filenames given on the command line as if Dafny were invoked multiple times
  • more attributes are passed through to Boogie
  • keyword "choose" is gone; use assign-such-that or let-such-that instead
  • various bug fixes

Reviews for this release

No reviews yet for this release.