dafny-lang/dafny v3.0.0-pre-release-0

Dafny 3.0.0 pre-release 0a

on GitHub

This is a pre-release of Dafny 3.0.0. It is stable, but does not yet have all the features slated for version 3.0. It has a long list of improvements over Dafny 2.3.0, though some of those improvements are not backward compatible with 2.3.0 (see "Breaking change" remarks below).

Here are the major changes since Dafny 2.3.0:

Language

• Allow datatype, codatatype, and newtype types to declare members (just like a class and a trait can declare members).

• Introduce :- statements and expressions.
  This new assignment operator extracts a successful value from the right-hand side (RHS) of the assignment, or propagates a failure if the evaluation of the RHS reports a failure. Some examples are in Test/exceptions/Exceptions1.dfy and Test/exceptions/Exceptions1Expressions.dfy.

• Introduce expect statements.
  The statement expect E, V; checks boolean expression E at run time and halts execution if it evaluates to false. The optional argument V is used in the error message produced. The verifier treats the statement as assume E;.

• Introduce :- expect (a.k.a. assign-or-halt) statements.
  This variation of the :- halts execution if the RHS reports a failure. Some examples are in Test/expectations/ExpectAndExceptions.dfy.

• Traits and classes that extend traits can now have type parameters.
  All occurrences of a trait among the ancestor traits of a class (or trait) must have the same type-parameter instantiations.

• Traits can now extend other traits.

• Order the cases of match statements/expressions.
  This allows overlaps between cases, where an earlier case gets selected first. A case can now also be just a variable (or _), which in effect is an "else". (Note, this is a backward compatible change, since no overlaps among cases were allowed before.) A warning is generated if one case is already covered by the preceding cases.

• Patterns in match cases can now use simple literal expressions, such as 2, 3.14, and false.

• Add full verification support for body-less loops.
  The loop targets of such a loop are the free mutable variables (including the heap) that occur in the guard, invariant, or decreases clause. If the loop has a modifies clause--whatever the modifies clause says--then the heap is counted as a loop target.

• Breaking change: In an export declarations, members of types are exported separately from exporting the type.

  • to export a member, the enclosing type must be provided or revealed
  • class constructors and mutable fields can be exported only if the enclosing class/trait is revealed
  • mutable fields can no longer be revealed, only provided
  • datatype constructors, discriminators, and destructors are exported when the datatype is revealed, and can never be explicitly named in exports
  • for an extreme predicate/lemma, the corresponding prefix predicate/lemma is exported, too

• Breaking change: New rules for exporting classes.

  To reveal a class or trait C will export:

  • the fact that this is a reference type
  • both types C and C?, and the connection between these two
  • the anonymous constructor, if C is a class and has one

  To provide a class or trait C will export:

  • the name C, as an opaque type
  • not type C?
  • no constructor or mutable field, and it's an error to explicitly name these in exports

  One breaking-change consequence of these rules is that constructor-less new is no longer supported for imported classes.

• The syntactic form import A.B.C is now allowed, and it stands for import C = A.B.C.

• import A.B.C`Xis now allowed.

• Introduce sequence construction expressions.
  Some examples are in Test/dafny0/Comprehensions.dfy.

• const fields are not allowed in back-tick notation in frames

• Allow import opened A where module A is in the same scope.

• Breaking change: Remove support for some deprecated syntax, and removed the keywords array1 and array1?.

• Breaking change: Make {: a token instead of two separate tokens.

• Breaking change: Disallow modify statements in forall statements.

• Breaking change: Don't support map disjointness, that is, a !! b is no longer supported when a and b are maps.

Verifier

• Improve representation of heap (as a map of map, rather than as 2-dimensional map).

• Fix refinement checks for two-state predicates.

• Don't re-verify code that comes from DLLs.

Compiler

• Add compiler to Java (fully featured, except iterator is not supported).

• Add initial version of a compiler to C++.

• Add support for {:test} attribute (C# only for now), mapping it to [Xunit.Fact]. This allows xUnit-like unit testing from Dafny.

• Compile forall statement into simple loop when possible.

• Compile tail-recursive functions (not just tail-recursive methods) with tail calls. For functions, the compiler has an auto-accumulator feature that automatically detects cases when an added accumulator variable allows the function to be transformed into being tail-recursive. In such detected cases, the compiler introduces the accumulator variable automatically.

• Enlarged support of {:extern} declarations

• Allow the compilation of collection types that take traits as type parameters.

• Compile methods with exactly one out-parameter to the usual result-type methods

• Compile map comprehensions with multiple bound variables.

• Support {:nativeType XX} where XX is a list of native types. They are considered in order and the first one supported by the compiler is picked. An error is generated if the type cannot be determined to fit in that native type. (See the /attrHelp message for details.) Also, number is no longer supported outside JavaScript.

• The .NET immutable collections that used to be used with the /optimize flag are now always used. The System.Collections.Immutable.dll library is no longer part of the Dafny distribution, since it is part of .NET. Also, /optimize flag is now permanently on, which causes /optimize flag to be passed down to the C# compiler.

• Introduce branch-coverage profiling. See new /coverage flag.

• Improved formatting of target code

• Breaking change: A number of features are now represented different at run time. This may break any previous external code that depended on the old representations.

Documentation

• Updates to the Dafny Language Reference Manual.

• For Dafny contributors, added documentation of compilation of trait/class to C#/Java/JavaScript/Go.

IDE

• End support of the DafnyExtension, which was the original Dafny IDE that plugged into Microsoft Visual Studio. (VS Code and Emacs plug-ins are still supported.)

Miscellaneous

• Various bug fixes throughout