Dafny 3.3.0

Dafny 3.3 makes many usability improvements. The language server, along with the next release of the VS Code plugin, offers better performance, displays informational message less like errors and more like hints, enlarges the repertoire of values that can be displayed for counterexamples, adds outlining features, etc.

Dafny 3.3 also adds a facility for generating test input. New language features include function by method, which allows a function to be implemented by statements, and ghost tuples.

Language

• Add function by method (see section 13.4 of the reference manual)

• Add ghost tuples: In addition to previous tuple types like (A, B, C), there is now an additional tuple type for each possibility of marking the components as ghost. For 3-tuples, that means the addition of the types (ghost A, B, C), (A, ghost B, C), (A, B, ghost C), (ghost A, ghost B, C), (ghost A, B, ghost C), (A, ghost B, ghost C), and (ghost A, ghost B, ghost C). There is still no non-ghost 1-tuple, but there is a ghost 1-tuple, (ghost A). The syntax for writing literal values of these types has ghost in front of the respective components. For example, (ghost 10, 12, ghost true) is a value of type (ghost int, int, ghost bool).

• Allow fresh to take an @-label

• Add ghost allocations. new can now be called in ghost contexts, which can be thought of as allocating the object in a special "ghost region" of the heap. A class can now declare a constructor to be ghost. Ghost constructors are used with ghost allocations of the class. The first phase of a ghost constructor is allowed to assign to both ghost and non-ghost fields of the class, but after that first phase, any non-ghost fields of the class are in effect readonly. Analogously, after a ghost new to allocate an array, the array's elements are in effect readonly. As part of this language addition, a ghost method is now allowed to allocate objects and arrays, but a lemma (lemma, twostate lemma, least lemma, greatest lemma) is still not allowed to do so.

Resolution, type checking, and type inference

• fix: Check type equality in override signatures

• fix!: Enforce non-nullness and allocatedness for unchanged

• Improve error location reported for bad break labels

Verifier

• The statement assume false; can now be used inside a loop body without turning the loop into a non-loop. Consequently, an assume false; inside the loop will not affect the verification of code outside the loop.

• Fix parallel assignment to const fields in constructor

• Fix :- assignment to const fields in constructor

• (internal) Verification stabilization: Use predecessor count instead of topological order index to determine function heights

• (internal) Verification stabilization: Use a hierarchical scheme for generating names of Boogie variables

• (internal) Emit captureState attributes in generated Boogie only when using /mv

• Miscellaneous bug fixes

Compiler

• Fix implementation of multiset operations related to zero multiplicity (C#, JavaScript, Go)

• Fix implementation of proper multiset-subset (Go)

• Fix compilation of superset operations

• Generate cleaner C# code

Documentation

• Remove mention of rise4fun.com, which is no longer available

• Miscellaneous fixes

IDE

• Improve performance

• Enable document outlines and the breadcrumb navigation at the top of the editor

• Do not display "Verified" for documents with parser/resolver errors

• Fix code suggestions in language server

• Add support for concurrent document updates

• Add language-server option to set the number of verifier cores

• Change the default info severity to hint. That is, the previous conspicuous blue underlines that were often confused for warnings or errors are now shown as some faint dots.

• Support verification timeouts in language server

• Fix language-server diagnostics for Windows

Tool

• Add /verificationLogger option, which records verification results for reporting and analysis

• Add /extractCounterexample option, which makes counterexample extraction accessible via the command line

• Add /warningsAsErrors

• Add /showSnippets, which displays a few lines of the offending source text

• Add test-generation facility, see https://github.com/dafny-lang/dafny/tree/master/Source/DafnyTestGeneration

• Improve pretty printing (import, and tuple arguments to functions)

• Use Boogie 2.9.6. Among other things, this means that dafny can be invoked with /errorTrace:0, which suppresses the display of the (for Dafny users mostly useless Boogie) execution trace.

• Make release builds when publishing Dafny

• Update use-local-boogie.sh to use .NET 5.0

Implementation

• Add an xUnit-based test runner for all of the lit tests under Test

• Fix nondeterminism in some tests (by serializing some tests and by increasing some time limits)

• Move source location of DafnyPrelude.bpl from Binaries to Source/Dafny

• Improve the use of pre-commit

• Add dafny-lang/libraries as submodule, to include its source code as integration tests

• Remove unnecessary solution configurations

• For Ubuntu build, use version 18.04

• Make it easier to run a local Boogie, see https://github.com/dafny-lang/dafny/wiki/INSTALL#build-against-a-custom-boogie

• Apply whitespaces formatting rules to entire codebase and run dotnet-format in the build

• Various code movement and refactoring; for example, breaking up Translator.cs into multiple files

• Simplify DafnyServer code by making it Dafny-specific, dropping ancient support for VCC and BCT

• Add an .editorconfig file to define the syntax style of the project

Dafny 3.3.0 pre-release 0

This is a pre-release of Dafny 3.3.0. Release notes are in development and may be included in subsequent pre-releases, and will at least be attached to the full 3.3.0 release.

Dafny 3.2.0

Dafny 3.2 introduces three new language features: run-time type tests for reference types (is), default parameter values, and for loops.

Language

• Permit as for reference types. For example, the expression a as object can be used to upcast an array a to type object, and o as array<int> can be used to downcast an object o to an integer array. There is a proof obligation that the expression evaluates to a value of the given type.

• Introduce is for reference types. For example, if C is a class that extends a trait Tr and t is a variable of type Tr, then t is C says whether or not the dynamic type of t (that is, the allocated type of t) is C. Any type parameters given in the target type must be uniquely determined from the static type of the expression; this maintains type parametricity in the language. Compilation support is provided for the C#, Java, JavaScript, and Go targets.

• Arguments to functions, methods, object constructors, and datatype constructors can be passed in not just positionally, but also by naming the parameter. For example, a call might look like GetIceCream(Vanilla, whippedCream := false, cherryOnTop := true).

• Allow parameters to be declared with nameonly, which says the parameter is not allowed to be passed in positionally.

• Allow parameters to be declared with a default-value expression.

• Introduce for loops. For example, you can now write

  for i := 0 to a.Length {
    print a[i];
  }
  

• Accept attributes in more places (e.g., on loops and cases).

Resolution, type checking, and type inference

• Fix method/function override detection.

• Fix omitted resolution of some attributes.

• Fix crash related to bitvectors.

Verifier

• Fix soundness issue where types were not cardinality-preserving.

• Improve/fix issues in matching-pattern expressions.

• Remove a matching loop in integer multiplication.

• Improve issues in dealing with function values.

• Fix bug that caused omission of some precondition checks.

• Fix omitted well-formedness checks on modifies and modify.

• Fix some malformed Boogie code.

• Additional bug fixes.

Compiler

• Compilation to Go sets flag to request pre-module behavior in Go. (In the future, the Go compiler will change to make use of Go modules.)

• For C#, fix rewriting of the name Main.

• Bug fixes for traits in Go.

• Tuple fixes in C++.

• Fix construction of large integers in Java.

• Fix comparison of some large integers in JavaScript.

• For C++, customize g++ warning settings and null printing based on underlying OS.

Documentation

• Some fixes.

IDE

• Upgrade the LSP Implementation of the Language Server.

Tool

• Make timeLimitMultiplier more specific.

• Fix and improve pretty printing.

Implementation

• In the compilers, TargetWriter is now named ConcreteSyntax. It has several new features for making it easier to generate well-formatted target code.

• Move some files into Verifier folder.

• Swap names Join and Meet.

Dafny 3.1.0

Dafny 3.1 is a minor update of Dafny 3.0. It mostly fixes some bugs, but it also adds some features.

Language

• feature: Allow invocations of two-state functions/lemmas to indicate which "old state" to use. The syntax is
  F@L(args), where F is the name of the function/lemma and L is a dominating label.

• feature: Let any type with members refine its members.

• Remove deprecated syntax NT(expr) for converting to a newtype NT. The current syntax is expr as NT.

Resolution, type checking, and type inference

• fix: Added missing consistency checks for type characterstics ((!new), (00), (0), (==)).

• fix: Check that all (ghost and non-ghost) const/var fields have initializers, when needed.

• fix: Disallow decreases * on ghost methods.

• If a * is used in a decreases or reads clause, no other expressions or *'s are allowed to be listed.

• Update type-inference algorithm: meets and joins are now considered before making decisions about arbitrary numeric types.

Verifier

• feature: Expand guessing of decreases clauses for while loops. The new guessing look at sets, multisets, and sequences, and the guesses may be lexicographic tuples. The most useful of these changes is probably that while s != {} gives rise to the guess decreases s.

• feature: Improve and expand auto-triggers for collections. Triggers for more expressions are now generated, so there will be fewer "no trigger" warnings. The changes also improve verifier performance for map comprehensions and fix some bugs.

• fix: Remove some unintended differences between receiver parameters and ordinary parameters.

• Fix encoding of map comprehensions.

• Fix issue with labeled heap states.

• fix: Detect and report Boogie out-of-resource errors.

• Miscellaneous bug fixes

Compiler

• Fix initialization of let-such-that bound variables.

• C#: Fix initialization issues related to extern opaque types.

• Java: Fix compilation of datatype constructors with only ghost parameters, and other issues.

• Java: Upon javac compilation failure, exit but don't crash.

• Go: Fix compilation of map update.

• C++: Support tuples with arbitrary arity.

• C++: Fix some path-related problems.

Documentation

• Minor improvements and fixed typos

Tool

• feature!: Add command-line option /stdin that reads standard input as if it were a .dfy file. Remove the old support for this, which had been to mention stdin.dfy on the command line.

• feature: Apply timeLimitMultipler to rlimit.

• Fix/improve some scripts

Implementation

• Merge Language Server sources. This will help us better keep versions and refactorings in synch.

• refactor: Improve UserDefinedType AST nodes by removing .ResolvedParam, and related changes.

Miscellaneous

• Various bug fixes throughout

Dafny 3.0.0

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

Dafny 3.0.0 Prerelease4

Language

• 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

Type checking

• Improve type inference for imported modules.

Resolution

• Enforce give type-characteristics for type synonyms and opaque types.

Verification

• Add /induction:4 option and make it the default. This new mode applies automatic
  induction to lemmas, but not to quantifiers. Use the {:induction} attribute to apply
  automatic induction to individual quantifiers.

Compilation

• Mature the support for Main methods. Check that the main method is unique, allow {:main}
  attribute, introduce /Main command-line switch.

• 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

• Improve Dafny Language Reference Manual.

Tool

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

Implementation

• Use .NET 5.0 version of Coco/R.

Dafny 3.0.0 PreRelease3

Language

• Allow empty types

• 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.
  Compilation support in 5 target languages (C#, JavaScript, Go, Java, C++).

• 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).
  Compilation support in 5 target languages (C#, JavaScript, Go, Java, C++).

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

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

Verification

• Pass fewer options to Z3.

• Add bitvector type axioms.

• Fix termination check for infinite/unknown types.

Compilation

• Clean up some Java runtime. For example, remove some unused methods. Also, rename some methods.

• Fix construction of maps in Java.

• Append “-java” to the name of the Java target folder. For example, compiling MyProgram.dfy
  to Java will create the target folder MyProgram-java.

Documentation

• Update Dafny Language Reference Manual

Tool

• Move from .NET Core 3.1 to .NET 5.0.

Miscellaneous

• Fix various bugs.

Dafny 3.0.0 PreRelease2

Publishing release 3.0.0-PreRelease2

Language

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

• Allow :- assignments to have multiple LHSs and corresponding RHS. Only the first value on the RHS is treated specially via its failure-compatible type.

• The :- can now optionally be followed by assert or assume, not just 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.

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

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

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

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

• Allow object in list of parent traits.

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

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

• 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 optional ; at the end of type and import declarations

Type checking

• Resolution and type checking is applied also in redundant case branches

• Include functions in datatype cyclicity checks

Verification

• Verify type members of opaque types

• Fix to subset checks for sequences

Compilation

• In the compilers to JavaScript and Go, support all co- and contra-variant type parameters.

• In the compilers to C# and Java, support co- and contra-variant type parameters, but not yet for datatypes.

• The previous C# and Java error message "not supported: trait as type parameter" is now emitted only for co- and contra-variant type parameters of. (This will also be removed when co- and contra-variant type parameters have been implemented for datatypes in these compilers.)

• Use type descriptors for C# (as was already done for Java, JavaScript, and Go). Update type descriptors for those other compilers, too (for example, rename _dafny.Type to _dafny.TypeDescriptor for Go, and similarly for Java). This fixes issues with auto-initialization.

• Fix some incorrect uses of nil in Go

• Fix array coercions in Java

• Fix eta-expansion of instance members

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

Documentation

• Many additions to the Dafny Language Reference Manual

• Some fixes in the rise4fun tutorial

Tool

• Migrate to .NET Core v2

  If you used to use mono Dafny.exe to run Dafny before, use dotnet Dafny.dll now. This is automated in the dafny script in the Binaries folder.

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

• Clarify -countVerificationErrors help message

• Improved error message for missing Z3

Implementation

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

Miscellaneous

• Various bug fixes

Dafny 3.0.0 pre-release 1

This version fixes some pre-release 0 issues with invoking the C# compiler on some platforms.

In addition, it has the following change from pre-release 0:

• Breaking change: Don't allow the use of bitvectors to state the desired length in array allocation and sequence construction
• Allow bitvectors as indices in single-dimensional arrays and sequences (just like they already were allowed for multi-dimensional arrays)

For the long list of other changes since version 2.3.0, see the 3.0.0 pre-release 0 release notes

Dafny 3.0.0 pre-release 0a

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