Syntax

Control flow

While

var a := new [2] (_ => 0);
var i : nat := 0;
while i < 10
  invariant i <= 10
  modifies a
{
  a[i] := i;
}

Nullable types

(from https://github.com/dafny-lang/dafny/releases)

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

Arrow types (Functions)

(from https://github.com/dafny-lang/dafny/commit/897c8e87bccc61464f54f4227a54075c7a581fd0)

A ~> B This is the most general arrow. It allows the function to have read effects (that is, have a reads clause) and allows it to be partial (that is, have a requires clause). This arrow was previously supported, but with the syntax A -> B.

A --> B This is the partial arrow. It does not allow read effects, but it allows the function to have a precondition. The type is a built-in subset type of the general arrow, that is, it is declared as follows (where I'm using its syntax and imagining that A and B are type parameters). type A -> B = f: A ~> B | forall a :: f.reads(a) == {}

A -> B This is the total arrow. It does not allow either read effects or preconditions. Note that the previous syntax -> now means a total arrow, not the general arrow. The total arrow is a built-in subset type of the partial arrow: type A -> B = f: A --> B | forall a :: f.requires(a)

Lambdas

reads and requires

var f := (x: ReferenceType) reads x requires WF(x) => Property(x)

Lambdas can reads their captured environment:

(from Test/dafny0/Comprehensions.dfy)

class SeqOp {
  var x: real
  
  function method S6(n: nat): seq<real>
    reads this
  {
    seq(n, i reads this => if i < 20 then 2.5 else x)
  }

Comprehensions

(from Test/dafny0/Comprehensions.dfy)

Sequence

var squares := seq(8, i => i*i);
assert |squares| == 8;
assert squares[6] == 36;

Set

function method Id(x: int): int { x }
var squares := set i | 0 <= i && i < 100 :: Id(i)*i;

Map

(from https://github.com/dafny-lang/dafny/releases)

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

Imperative code

(from https://github.com/dafny-lang/dafny/releases)

old@L(expr) and unchanged@L(frame_expr) expressions, which can refer to the value of the heap at an indicated statement label L.