dafny-lang/dafny v3.0.0-PreRelease3

Dafny 3.0.0 PreRelease3

on GitHub

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.