Skip to content

Dafny 2.1.1
Compare
Choose a tag to compare
@RustanLeino RustanLeino released this 10 Feb 06:44
· 3766 commits to master since this release
v2.1.1
0112e55

Version 2.1.1 is a minor update, mostly intended to return the correct version from the Dafny Server, so that the Dafny plug-in for VS Code can accurately offer advice about updating to the latest Dafny. In more detail, here are the changes from version 2.1.0 to version 2.1.1:

Language

  • Introduced old@L(expr) and unchanged@L(frame_expr) expressions, which can refer to the value of the heap at an indicated statement label L.

  • Labels, functions, and methods can now, like fields and (co)datatype destructors, have names that look like numeric integer literals.

  • Duplicate labels are no longer allowed when one of the labels dominates the other.

  • The continuity restriction for (co)inductive predicates has been relaxed. More precisely, there is no requirement of continuity for (co)inductive predicates using [ORDINAL] (which is also the default). The restriction applies only to predicates explicitly declared with [nat].

  • Abstemious functions: Allow functions to be annotated with {:abstemious}. Such a function is checked not to consume too much. More precisely, an abstemious function can only codatatype-destruct parameters and must return with a co-constructor.

    Abstemious functions, together with a new computation of a guaranteed minimum number of co-constructor wrappers, expand the number of functions that are considered to be productive. As a result, many new interesting co-recursive functions can be written.

  • When appropriate, try to give a hint about declaring a function to be abstemious.

  • Fewer restrictions on quantifiers over ORDINAL. Such quantifiers are now restricted only in the definition of (co)inductive predicates.

Verifier

  • More precise computations of when the heap is being used. This makes some logical encodings more efficient.

  • More knowledge about the exhaustive set of constructors of (co)datatypes. In particular, the new knowledge springs into being whenm two (co)datatype values are compared with equality or disequality. This makes it easier to prove programs that do direct comparisons rather than using a match construct.

IDEs

  • Make DafnyServer use the same version number as Dafny. This enable the Dafny plug-in for VS Code to accurately figure out when to offer to download the newest version of Dafny.

Build

  • Updated the Coco build and .exe to use VS 2017 and a .NET version 4.5

Miscellaneous

  • Some bugs fixes.
Assets 7
Loading