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

Dafny 2.3.0

The biggest change in version 2.3.0 from version 2.2.0 is the support of compilation to JavaScript and Go, in addition to the previously existing compilation to .NET. There are also some languages changes and other improvements, as described below.

Version 2.3.0 of Dafny requires the included Boogie version 2.4.1 and has been tested to work with Z3 version 4.5.0 and the included Z3 version 4.8.4.

Language

• Datatype updates are now allowed to update shared destructors. However, updates are now restricted to those that don't change the value's constructor. Also, updates where a candidate result constructor has anonymous parameters are no longer allowed. A precise description of datatype update is found in Test/dafny0/SharedDestructors.dfy, starting at line 65. Improved error messages and /rprint option for datatype updates.

• Added labeled assertion statements and labeled method/iterator preconditions. The syntax is like assert L: Expr; and requires L: Expr. The assumption that usually comes from an assertion or precondition is suppressed when these are labeled. To use the assumption, a reveal L; statement or expression must be used.
  See Test/dafny3/CalcExample.dfy for some examples.

• Labels, both in the statement label L: and in the new labeled assertions and preconditions, are now allowed to look like numeric literals (as was already allowed for field names and datatype destructors).

• reveal statements can now take a list of arguments.

• Allow more types with non-0 initializers to be passed as type parameters (supported by the compiler's
  new use of run-time type descriptors).

• Allow a module's submodules to be given in separate files: A module can now be declared with a qualified name. This is a just a syntactic shorthand for inserting the module into the indicated parent module. For example,

  module A {
    module B { }
  }
  

  must be written in one file, or else the curly braces won't match up. But these declarations can now be provided as:

  module A { }
  module A.B { }
  

  which allows A and A.B to be declared in separate files.

• A non-abstract module is not allowed to import or use (as in dereferencing the name of) an abstract module. However, any non-abstract module is allowed to contain or refine abstract modules.

Type checking

• Temporarily, added a {:termination false} attribute that can be placed on trait declarations to unsoundly ignore termination checking for dynamic method dispatch that goes to other modules. A better and sound solution will come in the future.

• Various bug fixes

Verifier

• Added specialized (extensional) equality for inductive datatypes.

• Various bug fixes

Compiler

• Compilation now targets not just .NET (via C#), but also JavaScript and Go. These are selected with the command-line switch /compileTarget:<language>, where <language> is one of cs, js, or go.

• For compilation to JavaScript, also accept files with extension .js on the command line.

• Improved {:extern} for methods and function:
  {:extern} says to use the Dafny method name as the external name.
  {:extern "M"} and {:extern "Q", "M"} say to use M as the external name.
  In the 0- and 1-argument forms, qualified forms of the method name are constructed according
  to the enclosing class and modules in Dafny (and those enclosing declarations may have
  :extern attributes themselves, which are be taken into account).
  In the 2-argument form, Q.M is used as the qualified name and the names of enclosing classes
  and modules are not consulted. If needed, Q can contain dots; for example,
  {:extern "R.S.T", "M"} will cause the qualified name of the extern to be R.S.T.M.

• An {:extern} constructor is now called using C#'s constructor mechanism.

• Improved {:extern} for modules:
  {:extern} says to use the module name as the extern name.
  {:extern "N"} says to use "N" as the extern name.
  {:extern "N", "L"} for JavaScript says to use "N" as the extern name and to initialize it to
  require("L").
  For compilation to Go, {:extern ""} indicates Go's built-in "module", which contains types
  like error. (For more information about using externs with Go, see Docs/Compilation/Go.md.)

• Support for interacting with C code on .NET. The {:dllimport} attribute translates to the .NET DllImportAttribute. Attribute {:handle} can be placed on some reference types to cause their translation to turn into uninterpreted machine words.

• Deprecated extern keyword. Use the {:extern} attribute instead.

• Allow program entry point (Main method) to take any number of ghost in- and out-parameters.

• Added command-line option /compile:4, which is like /compile:3 but compiles/runs regardless of how the verification turned out.

• Added command-line option /compileVerbose, which can suppress some information compiler output.

• Removed the struct that was previously used in the C# compilation of datatypes. Also, compilation of datatypes with only one constructor are special-cased.

• Renamed tuple types in the compiled code to something more straightforward and human readable.

• Improvements in identifier-protection schemes (which avoid clashes with keywords in the target language).

• Compilation to C# uses /nowarn:0168 to suppress warnings about unused variables under Mono.

• Improved printing of real numbers.

• Various improvements in compiled code.

• Various bug fixes

Dafny 2.2.0

Version 2.2.0 differs over version 2.1.1 in the following ways:

Language

• In abstract modules, const declarations are allowed to omit initializing expressions,
  even if it is not known how to initialize values of its type.

• Variables introduced in pattern-matching var statements are now mutable, like
  other local variables.

• Added general map comprehensions, of the form map x,y | R(x,y) :: f(x,y) := g(x,y).
  This map takes f(x,y) to g(x,y), where x and y are any values that satisfy
  R(x, y). The ordinary map comprehension map x | R(x) :: g(x) is a special case
  of the general map comprehension map x | R(x) :: x := g(x).

• Collection types (sets, sequences, multisets, and maps) and many varieties of
  inductive datatypes are now considered as having a zero initializer. This includes
  string, which is a synonym for seq<char>.

• Syntactic heuristics for detecting finite sets consider equalities.

• Possibly-null array-type names are now keywords (e.g., array?).

• An expression of the form exists x :: A ==> B, which is almost always a mistakes,
  now generates an warning. Use parentheses around the quantifier body to override.

Verifier

• New default encoding of non-linear arithmetic (/arith:1). Also added various
  experimental modes (/arith switch) that are subject to change in the future.

• Various bug fixes.

Compiler

• New /spillTargetCode modes 2 and 3, which write out the .cs file without
  invoking the C# compiler

• Turn off warning 0162 (unreachable code)

• Fixed equalities-checking bug.

Miscellaneous

• Improvements in Linux and MacOS run script

• Various bug fixes

Dafny 2.1.1

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.

Dafny 2.1.0

Dafny version 2.1.0 mainly introduces non-null types, more precise type inference in the presence of subset types, full checks that functions do not depend on the allocation state, and an expanded selection of variance annotations. Some of these changes are not backwards compatible, but the changes required to bring older programs up to version 2.1.0 are usually not large.

Another change is that Visual Studio support has been moved to VS 2017, .NET version 4.5. Building under Mono still works, but only without using Code Contracts (which don't seem to be available on Mono).

In more detail, the changes over version 2.0.0 are as follows:

Language

• Non-null types.

  A declaration of a class or trait C gives rise to two types, C? and C.

  Type C? is the possibly null reference type for C objects. Previously in Dafny, this was the only type the class or trait gave rise to and it then had the different name C.

  Type C is a non-null version of C?. It is a defined as the subset type:

  type C = c: C? | c != null
  

  Note that the ? is part of the name of the class C?. It is not a suffix operator, so there cannot be any space between the C and the ?. Also, if a class C has type parameters, then these are mentioned after the type names C? and C, for example, C?<int> and C<int>.

  In some places in the program text, a class or trait name is expected. In particular, a trait name is expected after the extends keyword in a class declaration and a class name is expected in a new allocation. Note that these names, because they are class and trait names, not type names, do not end with a ?.

• Dafny has a built-in trait object and any number of built-in array classes (array, array2, array3, ...). Each of these also gives rise to two types, as in object? and object, array? and array, array2? and array2, etc.

• If the literal null is compared with an expression of a non-null type, Dafny will emit a warning that the result of the test can be determined at compile time. For example, if p has a non-null type and S is a set whose element type is a non-null type, then both p != null and null in S will generate said warning.

• The subset types declared in a program form a hierarchy (that is, a tree), where the parent of a subset type is its given base type. This hierarchy is part of the subtype relation in Dafny. For example, nat is a subtype of int, and for any class or trait C, C is a subtype of C?. In addition, for every class or trait C that extends a trait Tr, type C? is a subtype of Tr? and type C is a subtype of Tr.

  As a consequence of these rules, note that the subtype relation is not just a hierarhcy.

  Suppose X is a subset type whose base type is C. It then follows that X is a subtype of C, which in turn is a subtype of C?. However, the declaration of X only gives rise to one type. In particular, it does not also give rise to a type X?. In other words, any user-defined subset type of C? or C is only a subtype of it.

• Type inference is now more precise. Whereas before it would not infer subset types like nat or --> (but instead their base type, int and ~>), now it will try to infer such types. In some cases, this will not make a noticeable, but there are two cases where the difference may be important.

  One case is that type arguments more easily will be inferred as subset types. For example, suppose the usual datatype List has a co-variant type parameter and suppose xs is a variable declared to have type List<nat>. Expression Cons(55, xs) may now be inferred to have type List<nat> as well. This is beneficial for verification, because in an assignment like xs := Cons(55, xs);, the verifier only needs to check that 55 satisfies the constraint of nat. Previously, it was more likely that Cons(55, xs) would be inferred to have type List<int>, in which case the assignment xs := Cons(55, xs); put the burden on the verifier to check that Cons(55, xs) produces a value that actually satisfies List<nat>.

  The other case where the more precise type inference can make a noticeable difference is in comprehensions like quantifications and set comprehensions. Suppose P is a predicate declared to take a parameter of type nat and consider an expression forall x :: P(x) ==> 0 <= x. If x has type nat, then this quantifier is a tautology. If x has type int, then the expression is not well-formed, because the subexpression P(x) would not satisfy the type conditions of P. For this example, Dafny will infer the type of x to be nat.

  As another example, of a quantifier, suppose P and Q are both predicates that take a nat argument. Then, Dafny will infer x to have type nat in forall x :: 0 <= x && P(x) ==> Q(x) as well. So, in this example, since x is inferred to be of type nat, the antecedent 0 <= x is redundant and can be omitted.

  As a third example, suppose neg is a subset type of int that stands for the negative integers, P is a predicate that takes an argument of type nat, and Q is a predicate that takes an argument of type neg. Consider the following expression:

  forall x :: (0 <= x ==> P(x)) && (0 < x ==> Q(x))
  

  For this expression, Dafny will infer that x has type int. In an alternative design, inference might have resulted in the type nat or neg, each of which would render one of the conjuncts trivially satisfied, or resulted in error message like "overconstrained type".

• Allow more RHSs of const declarations.

• The possible variance indicators on type parameters has been expanded. The possibilities are:

  • + (co-variance, strict)
    Enclosing type is monotonic in the type parameter.
    The parameter is not used in expanding positions (that is, it is not used left of any arrow).

  • * (co-variance, relaxed)
    Enclosing type is monotonic in the type parameter.
    Other than that, use of the parameter is unrestricted (in particular, it may be used to the left of an arrow).

  • (default variance, denoted by not giving any of the other variance indicators explicitly) (non-variance, strict)
    Different given parameters produce non-comparable types.
    The parameter is not used in expanding positions (that is, it is not used left of any arrow).

  • ! (non-variance, relaxed)
    Different given parameters produce non-comparable types.
    Other than that, use of the parameter is unrestricted (in particular, it may be used to the left of an arrow).

  • - (contra-variance)
    Enclosing type is anti-monotonic in the type parameter.
    Consequentially, every use of the parameter is to the left of some arrow.

• Strict positivity is used to forbid type definitions where differences in cardinalities would give rise to a logical contradiction.

• Added type-parameter characteristic (!new), which says that the type does not include any references, and thus does not depend on the allocation state. It can be used to restrict type parameters so that functions can use the type in unbounded quantifications.

• Opaque types at the very topmost scope are always implicitly (!new).

Verification

• Support for customizable error messages (useful for tools built on top of Dafny).

• Removed the notoriously bad seq axiom. (More precisely, rewrote it to have a good trigger.)

• Some performance improvements.

• Improved and expanded on the syntactic bounds discovery in comprehensions.

IDE

• Visual Studio mode is for VS 2017

Compiler

• Some bug fixes, for example to work around some questionable designs around the use of null in the .NET collection libraries.

Command-line options

• Command-line option /titrace spills out debug trace information from the type inference process. Previously, this debug trace information was hidden under an #if, but now it can be turned on without having to recompile Dafny.

• Added /noExterns flag, which ignores :extern attributes.

• Started implementing a /allocated:4 mode.

Miscellaneous

• Include Code Contracts for VS 2017. This requires Code Contracts to have been installed (for some version of Visual Studio, like VS 2015) on the machine.

• Various bug fixes.

Dafny 2.0.0

Dafny version 2.0.0 introduces a number of language improvements. Some of these
are not backwards compatible, but the changes required to bring older programs
up to version 2.0.0 are not large. In more detail, the changes over version 1.9.9
are as follows:

Language

• Added witness or ghost witness clause to newtype and subset-type declarations.
  This lets program supply a hint that shows the declared type to be nonempty.
  Such types are now supported.

• Array allocation now supports a parameter that says how to initialize the
  newly allocated elements.

• Added array display expressions, that is, array allocations where the initial
  elements are given by a (sequence-looking) display.

• If the type or size of an array allocation are omitted, Dafny tries to infer these

• Type synonyms and subset types now, like other type declarations, support type
  parameters marked with the characteristic (==). This mark restricts the type
  parameter to types that support equality tests in compiled code. Such (==)
  marks are inferred from the right-hand sides of type declarations, except when
  the right-hand sides have different visibility than the type being declared.

• const declarations (that is, read-only fields, or call them final fields) are
  now allowed in classes and traits. Like field declarations, const declarations
  in a class or trait are per-instance. A const declaration in a class or trait
  can be marked static (previously, all const declarations in classes and
  traits were implicitly static; this has now changed).

• The type or initial value, but not both, of a const can be omitted.

• A static const without an initial value stands for an underspecified constant.
  An instance const whose declaration does not give an initial value can
  optionally be assigned a value inside constructors.

• The extern keyword has been deprecated. Instead, use the {:extern} attribute.

• A constructor in a class is now implicitly allowed to modify the fields
  of this and the constructor's precondition is not allowed to mention this.
  (Previously, a constructor had been much more like a method, but with
  the restriction that the constructor could only be invoked as part of a new
  allocation. Thus, constructors previous had required a modifies this clause.
  Listing this in a modifies clause of a constructor now produces a
  deprecation warning.)

• The body of a constructor in a class is now divided into two parts. The
  first division is responsible for setting the values of const fields, but
  can also set the values of mutable fields of the object. The second division
  is not allowed to assign to const fields, but can assign to the object's
  mutable fields.

  The use of this is restricted in the first division. It can
  be used (implicitly or explicitly) in the left-hand side of assignments of
  the fields of this (for example, this.x := 10;). Moreover, in such an
  assignment, the right-hand side is allowed to be this or (with this
  being implicit or explicit) this.x (for example, this.x := this.y;
  and this.next := this;). These are the only allowed uses of this in
  the first division. (Actually, there is one more special case: any instance
  const whose declaration includes an initial value is allowed to be mentioned
  freely anywhere in the constuctor. Such a const is never allowed an assignment
  by a constructor.)

  The two divisions are separated by the statement new;, which can only be used
  at the top level of the constructor's body. If a constructor body does not explicitly
  include the division-marker statement new;, then there is an implicit new;
  and the end of the body; in other words, if there is no new;, then the entire
  constructor body denotes the first division.

  The first division is not allowed to use any return statement.

• At the end of the first division of each constructor in a class, all fields
  must either have been assigned values or must be of a type that allows zero
  initialization. A class that contains a field that cannot be zero initialized
  must have at least one constructor.

• Any local variable or out-parameter whose type does not allow zero initialization
  is subject to a definite assignment rule. This means that any use of the
  variable must have been preceded by a definition. Unlike Java and C#, which
  enforce their definite-assignment rules syntactically, Dafny enforces its
  rule semantics (that is, it is the verifier that enforces the rule). There is
  an implicit use of every out-parameter upon return from from method.

• Type parameters and opaque-type declarations can use the new characteristic (0),
  which restricts any instantiation of the type with types that support zero
  initialization. All type parameters of an iterator automatically and
  unavoidably get the (0) characteristic (doing otherwise would require a
  fancier design of the initialization of iterators).

• There are now three built-in arrow-type constructors: ~> is the general arrow,
  which allows read effects and partiality. That is, the functions that general
  arrows stand for can be have reads and requires clauses). --> is
  the partial arrow, which allows partiality, but no read effects. That is,
  the functions that partial arrows stand for can have requires clauses.
  -> is the total arrow, which allows neither read effects nor partiality.
  That is, the functions that total arrows stand for can have neither reads
  clauses nor requires clauses. In previous versions of Dafny, there was only
  the general arrow and it had the syntax ->, which is now used by the total
  arrow.

  The partial arrow is a built-in subset type with ~> as its base type,
  and the total arrow is a built-in subset type with --> as its base type.
  That is, it is as if --> and -> were declared as follows (here shown
  for arrows with arity 1):

  type A --> B = f: A ~> B | forall a :: f.reads(a) == {}
  type A -> B = f: A --> B | forall a :: f.requires(a)
  

  The new arrow types are treated specially. In particular, the resolver knows
  that --> and -> have no read effects, so the verifier does not need to
  check these. This gives rise to cleaner specifications of functions.

• Type-parameter variance is now user definable, using a prefix +, -, or =.

• Added type ORDINAL, standing for all ordinals in the mathematical world.
  The type supports integer literals, + and -, and relational operators.
  There are restrictions on where ORDINAL can be used. It is not allowed in
  some quantifiers and it can never be passed as a type parameter.

• The iterates of extreme predicates can now be indexed by ORDINAL instead
  of nat. By default, it uses ORDINAL, but either can be selected by
  following the name of the extreme predicate, in its declaration, by either
  [ORDINAL] or [nat].

Verification

• Automatically compute matching triggers for more kinds of quantifier expressions,
  including quantifiers that use let expressions.

• For a calculation that begins or ends with certain "top" or "bottom" literals
  (like true or false for type bool), the default calc operator is not
  chosen to be ==, but rather only "half" of this equality (that is, ==>
  or <== for booleans, or >= or <= for some other types). Since the other
  direction of the calculation as a whole follows trivially, this can make
  verification more efficient.

• Reads checks on newtype and subset-type constraints now happens under the
  assumption of the constraint itself.

• The heap variable is now used frugally in the encoding of functions. (This is
  done by default, but previous encodings are available via the /allocate
  command-line option.)

• The supported version of Z3 is now 4.5.0.

IDE

• Support for VS Code.

• Syntax highlighting for new keywords in Visual Studio.

• Produce hover text to indicate that if/while/match statements are ghost.

• Hover text shows main operator in calc statements.

• Fixed annoying problem in Visual Studio that had caused a crash when a .txt
  file was saved as a .dfy file.

Compiler

• Suppress internal warning about variables assigned to themselves.

• Suppress internal warning about unreachable code generated by the Dafny compiler.

• Forbid some uses of traits as type parameters when doing so might require
  expensive run-time tests.

Command-line options

• /definiteAssignment allows some customized behavior of the definite-assignment
  rule. One mode of this switch can forbid programs from using potentially
  nondeterministic statements.

Miscellaneous

• Improved source locations in some error messages.

• Various bug fixes and improvements.

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.