dafny-lang/dafny v2.0.0

Dafny 2.0.0

on GitHub

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.