Introducing Dafny 3.0!

Highlights

Here are some of the exciting changes since Dafny 2.3.0:

• Full compilation support to target C#, JavaScript, Go, and Java, and some support to target C++. (Fine print: C# and Java targets do not yet support type-parameter variance for datatypes. The Java target does not support Dafny's iterator declarations.)

• Datatypes, co-datatypes, newtypes, and opaque types can declare members (methods, functions, constants), just like classes and traits.

• Traits and classes that extend traits can have type parameters.

• Types can be empty. Subset types and newtypes can opt out of giving a witness.

• Type parameters and opaque types can be declared to require auto-initialization or non-emptiness.

• The cases of match constructs are ordered, and case patterns can include simple literal constants.

• expect statements ("check-or-halt") introduce assumptions that are checked at run time.

• :- assignments ("assign-or-return") provide abrupt return from a method upon failure (cf. exception handling). Similarly, :- let-bindings give expressions a way to handle failures (cf. monads).

• There are sequence comprehensions, map comprehensions are more expressive, and operators for map merge and map domain subtraction.

• Substantial refresh of the Dafny Language Reference Manual.

• Co-released with a new Dafny plug-in for VS Code.

Details

Here is a detailed list of the major improvements since Dafny 2.3.0. Some of these improvements are not backward compatible with 2.3.0, as noted by "Breaking change" tags.

Language

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

• There are expect statements ("check-or-halt").

  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;.

  The statement can be used in statement expressions. For example, expect 0 <= i < a.Length; a[i] returns element i of a, but halts if i is not in range.

• There are :- statements ("assign-or-return") and expressions ("let-or-fail").

  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.

  The :- constructs can have multiple LHSs and corresponding RHSs. Only the first value on the RHS is treated specially via its failure-compatible type.

  The :- is optionally be followed by assert, assume, or expect. Each of these makes a claim about the success of the operation (i.e., assert !r.IsFailure();, assume !r.IsFailure();, expect !r.IsFailure();). When any of these keywords is used, there is no requirement for the failure-compatible type to have a PropagateFailure() member, since it will not be used.

• Traits and classes that extend traits can 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 extend other traits.

• Permit object in list of parent traits.

• Allow assignments c := t; where the type of t is a parent trait of the type of c. This gives a way to cast a trait to a class. However, this is not a type test and the verifier will check that the value of t really does satisfy the type of c.

• The cases of match statements/expressions are matched in the order given.

  This allows overlaps between cases, where an earlier case gets selected first. A case pattern can 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 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 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 or 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

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

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

• import A.B.C`Xis allowed.

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

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

• Allow bitvectors as indices in single-dimensional arrays and sequences (just like they already were allowed for multi-dimensional arrays).

• Breaking change: Don't allow the use of bitvectors to state the desired length in array allocation and sequence construction.

• Allow empty types.

• A subset type or newtype now supports the following witness clauses:

  • witness E says that E is a compiled expression that is a value of the type
  • the absence of a witness defaults to
    -- witness 0 for types based on integers or bitvectors,
    -- witness 0.0 for real-based types,
    -- witness {} for set-based types,
    -- etc.
  • ghost witness E says that E is a ghost expression that is a value of the type
  • witness * opts out of witness checking; instead, the type is treated as being possibly empty

• Update meaning of the (0) type characteristic. Each type now falls into one of three categories:

  • Auto-initializing, denoted by the type characteristic (0). The type is known to have a compilable value. This lets variables in compiled contexts be used before initialization.
  • Nonempty, denoted by the type characteristic (00). The type is known to have at least one possible value. This lets variables in ghost contexts be used before initialization. In compiled contexts, a variable of this type is subject to definite-assignment rules (which means the variable must be assigned before any use).
  • Possibly empty, denoted by the absence of (0) and (00). This restricts use of variables of the type, making them subject to definite-assignment rules in both compiled and ghost contexts.

• Introduce map merge operator (syntax m0 + m1), whose keys are the union of the keys of m0 and m1, and which for the keys in m1 associates the same values as in m1 and for the other keys associates the values of m0. Works on both map and imap, but both arguments must be the same.

• Introduce map domain subtraction operator (syntax m - s), which is like map m but without any key in set s. Operand m can be either a map or imap, but s can only be a set (not an iset).

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

• Breaking change: Rename inductive predicate, copredicate, inductive lemma, and colemma to least predicate, greatest predicate, least lemma, and greatest lemma, respecitvely. Deprecation warnings are emitted upon coming across the old syntax. In each of the 4 cases, the new syntax is a reserved keyword phrase. However, least and greatest are not reserved keywords by themselves.

• Fix some inconsistencies in the grammar. For example, be more consistent about where digit names and names beginning with an underscore are allowed.

• Improved name resolution.

  • Imported types with the same name are not considered ambiguous if they refer to the same type .
  • Allow C. to refer to a datatype constructor, but only if C does not resolve to anything else.
  • Allow import A.B even without import A.

• Breaking change: {: is now one token, not two separate tokens.

• Breaking change: Disallow modify statements in forall statements.

• Breaking change: Removed some deprecated features that have been marked as deprecated for a long time.

  • int(_) and real(_) conversions
  • parallel, comethod, free, and protected keywords
  • the keywords array1 and array1?
  • the optional ; at the end of type and import declarations

Resolution, type checking, and type inference

• Include functions in datatype cyclicity checks.

• Improve auto-ghost declarations of local or bound variables: if the variable is declared with an initializing RHS and the RHS requires the variable to be ghost, then it is made ghost even if the declaration uses var (as opposed to uses ghost var).

• At the module scope, prefer local names over opened-imported names.

• Through constant folding, detect more constant bounds in type declarations. For example, given const UINT32_LIMIT := 0x1_0000_0000, the declaration newtype uint32 = x | 0 <= x < UINT32_LIMIT is allowed.

• Allow negative literals for integer- and real-based types. More precisely, a - token follows by a digits-token is interpreted as a negative literal for integer- and real-based types. case-patterns in match constructs can use these negative literals. For bitvectors, such a - is still considered a unary-minus expression. For ORDINAL, such a - would be unary minus, but ORDINAL does not support unary minus, so it's an error.

• Allow a refinement module to extend members of all types that can have members, not just classes.

• Improve type inference for imported modules.

• Enforce any declared type-characteristics for type synonyms and opaque types.

Verifier

• Breaking change: The new /induction:4 option is the default for automatic induction. This new mode applies automatic induction to lemmas, but not to quantifiers. Use the {:induction} attribute to apply automatic induction to individual quantifiers.

• 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.

• Fix to subset checks for sequences.

• Add bitvector type axioms.

• Fix termination check for infinite/unknown types.

Compiler

• Compiler that targets Java. Does not support iterator declarations, and does not yet support variance for (co)datatype type parameters.

• Prototype compiler that targets C++.

• Improved support for and consistency among the compilers that target C#, JavaScript, and Go.

• Expanded entry points: The main method (named Main, marked with attribute {:main}, or specified using the /Main command-line option) can be a module method or a static or instance method in a class, trait, (co)datatype, or newtypes (provided the type is auto-initializing or a class with no constructor declarations).

• Support type-parameter (co- and contra-)variance for collection types (C#, JavaScript, Go, Java), and support type-parameter variance for (co)datatypes (JavaScript and Go). Traits can be used as type parameters (for JavaScript and Go, everywhere; for C# and Java, as non-variant type parameters.)

• Compile map comprehensions with multiple bound variables.

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

• Optimize forall statements 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.

• There's some rudimentary support for collecting branch-coverage information at run time (see /coverage command-line option, and see Test/comp/BranchCoverage.dfy for an example).

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

• Enlarged support of {:extern} declarations, improving the foreign-function-interface to other languages.

• 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, native type "number" is no longer supported outside JavaScript.

• Always use .NET immutable collections (previously, these were used only with the /optimize flag). Also, /optimize flag is now permanently on, which causes /optimize flag to be passed down to the C# compiler.

• Improved formatting of target code

• Breaking change: A number of features are now represented differently at run time. This may break any previous external code that depended on the old representations. (Here's one hint: If you handwrite target code that creates datatype values, use the create_ methods, don't call new directly.)

• Use run-time type descriptors for C# and Java, as was already done for JavaScript and Go. This adds uniform support for auto-initialization, and removes from Dafny the previous notion of "zero-initializable types".

• Fix some incorrect uses of nil in Go.

• Fix eta-expansion of instance members.

• Fix name-capture problems in lambdas, quantifiers, set/map comprehensions, and tail-recursive functions/methods.

• Make /compile and /spillTargetCode command-line options work consistently for the 5 compilers: C#, JavaScript, Go, Java, C++. The /compile option controls whether or not an executable target is generated, and also controls whether or not to run the program upon successful compilation.

  • Option /compile:0 generates no executable target.
  • Option /compile:1 generates an executable target that can be run.
  • Option /compile:3 compiles and runs the program, but doesn't generate an executable target unless necessary for running.

  The /spillTargetCode option controls whether or not textual target code is generated. This can be useful if the Dafny program is to be manually compiled with handwritten code in the target language.

  The test file Test/comp/compile1quiet/CompileRunQuietly.dfy shows how to run the executable target generated by Dafny.

  The test file Test/comp/manualcompile/ManualCompile.dfy shows manual compiler calls that can be applied to the textual target code generated.

Documentation

• Large refresh of the Dafny Language Reference Manual.

• Some fixes in the rise4fun tutorial.

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

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.)

Tool

• Migrate to .NET 5.0.

  If you used to use mono Dafny.exe to run Dafny before, use dotnet Dafny.dll now. If you used the dafny script before, use the updated version with the same name. If you're building from source, you'll find the dafny script in the Scripts folder, and you may want to copy it to the Binaries folder. See INSTALL instructions in the wiki.

• Allow and ignore duplicated filenames on the command line and via include directives. Such duplicates are determined using case-sensitive canonical path names.

• Improved error message for missing Z3.

• Deprecate -countVerificationErrors command-line option.

• Retire /ironDafny and /dafnycc command-line options.

Implementation

• Use Boogie v2.8.26.

• Use Z3 v4.8.5.

• Pass fewer options to Z3.

• Use .NET 5.0 version of Coco/R.

• Various refactorings to improve code structure, especially across the compilers.

Miscellaneous

• Various bug fixes throughout