Dafny 1.9.9

Dafny version 1.9.9 includes the following changes over version 1.9.8:

Language

• Allow TLA+ style conjunctions and disjunctions.

• Allow the first datatype constructor to be preceded by a |.

• Destructor names can now be shared among datatype constructors.

• Added two-state functions and two-state predicates.

• Two-state lemmas no longer support reads clauses. Instead, use the new unchanged predicate.

• Added unchanged predicate, which takes a frame argument and says those things are the same in the pre- and post-states.

• fresh applied to a collection now says that all elements of the collection are fresh. This is a change in semantics from before.

• allocated predicate (re-)introduced. It says that its argument is available in the state.

• Inside an old, disallow unchanged, fresh, two-state functions, two-state lemmas, and nested old.

• Added const declarations.

• Added conversions between char an integral types.

• Function results can now be named, for use in the function's postcondition.

• Added operations that rotate bits in bitvectors.

• map and imap now have .Keys, .Values, and .Items members.

• Language support for revealing {:opaque} functions. Use reveal F() instead of the previous reveal_F().

• Support for tuples in match constructs.

• Expand the repertoire of constructs where co-recursive function calls are recognized.

• Proper support for type parameters in inductive and co-inductive predicates.

• Allow reads clauses on inductive and co-inductive predicates.

• Disallow parameters marked with ghost in signatures that are already ghost.

Modules

• Class members can be individually exported.

• Datatypes can now be exported as provided or revealed.

• All datatypes can be revealed by reveal *.

• Opened imports are not exported.

• exclusively refines is no longer supported.

• Module facades may now only be refined by explicit refinements. The previous structural checks are no longer supported.

Verification

• Improved string support

• More quantifier rewriting to help avoid matching loops, in particular address quantifiers like forall i :: 1 <= i < a.Length ==> a[i-1] <= a[i]

Pipeline

• Speed-ups in resolution and translation (and added /optimizeResolution flag).

• Set appropriate exit value for Dafny errors.

• Use .NET Framework 4.5.

IDEs

• Syntax highlight bitvectors in Visual Studio.

• Show some Boogie resolution errors in lieu of many a "Verification process error" in Visual Studio.

• Improved caching.

Advanced settings

• Improvement in manual fuel settings.

• /allocated option, which encodes allocatedness in alternate ways.

• /printIncludes option.

• /disableScopes option.

• Handle :warnShadowing attribute on methods and lemmas.

• As an optimization, Boogie implementations with no proof obligations are no longer emitted.

• Don't verify modules that came from an include.

Miscellaneous

• Bug fixes in subset types.

• Various bug fixes, including many Issues reported on github.