1.1 Statements🔗

• Declaration:

  var i: int;
  var i: int := 5
  var j: real;

• Assignment:

  i := 5;
  i :| i > 0; //Choose some value for i such that the condition i > 0 holds.
  f :- Find(5); //assign to f some result value that satisfies the 
                // postconditions of Find with the given arguments.
  i, j, k := k, j, i;
  i, j, k := m();
  i := *; // i is now some arbitrary int

  Dafny

    method Find(x: int) returns (y: int)
    ensures y > x
  {
    y :| y > x;
  }
  
  method Test() {
    var i := Find(5);
    assert i > 5;
  }

• Method Call:

  m(5,6,7);
  i, j, k := p(5,6,7);
  i, j, k :- p(5,6,7);

• Conditional:

  if … { … } else …
  if x: int | P(x) { … } else …
  if case … => … case … => …
  match s case p => … case q => …

• Loop:

  while … { … }
  while case … => … case … => …
  for i: int := … to … { … }
  for i: int := … downto … { … }
  break;
  continue;

• Labeled:

  label L: …

• Forall:

  forall i | 0 <= i < j { … }
  forall e <- s { … }

• Others:

  { … }
  return ;
  return …, …;
  yield ;
  yield …, …;
  assert … ;
  assume … ;
  expect …, msg ;
  print …, …, …;
  reveal …, …, … ;
  modify …, …, … ;
  calc <= { … ; … ; … ; }

1.2 Expressions🔗

• Logical Operators:

  <==> ==> <== && || !

• Comparison operators:

  == != < <= > >= !! in !in

• Infix and Unary operators:

  + - * / % | & ^ ! << >>

• Conditional:

  if … then … else …
  match … case … => … case … => …

• Tests and Conversions:

  e is Type
  e as Type

• Lambda expression:

  i => i*i
  (i, j) => i+j
  (i: int) requires … => …
  (i: int, r: real) => …

• Allocations:

  new MyClass
  new MyClass(4,5,6)
  new MyClass.Init(5,6,7)
  new int[10]
  new int[][5,6,7,8,9]
  new int[5](_ => 42)
  new int[10,10]((i,j)=>i+j)

• Collections:

  [ e1, e2, e3 ]
  seq(n, i requires 0<=i<n => f(i))
  { e1, e2, e3 }
  iset{ e1, e2, e3 }
  set x: nat | x < 10 :: x*x
  multiset{ e1, e2, e3 }
  multiset(s)
  map[ 1:= ‘a’, 2 := ‘b’ ]
  map x: int | 0<=x<10 :: -x := x
  m.Keys m.Values m.Items

• Two-state:

  old(o) old@L(o)
  allocated(o) allocated@L(o)
  unchanged(o) unchanged@L(o)
  fresh(o) fresh@L(o)

• Primaries:

  this null true false
  5 0.0 0xABCD ‘c’ "asd" @"asd"
  ( e )
  | e |
  e.f
  e.fn(3,4,5)
  e.fn(3,4,option:=5)

• Arrays & sequences:

  a[6]
  a[j..k] a[j..] a[..k] a[..]
  s[ 2 : 2 : 2 : ]

• Updates:

  d.(f := x)
  s.[ 2 := 6, 3 := 7]
  mp.[ 2 := "Two", 3 := "Three"]

• Quantifiers, Let expressions:

  forall x: int :: x > 0
  exists x: int :: x > 0
  var k := j*j; k*k
  var k :| k > 0; k + 1
  var k :- f(); k + 1
  var R(x,y) := T(); x+y

• Statements in expressions:

  assert P(x); x > 0
  assume P(x); x > 0
  expect P(x); x > 0
  reveal … ; x > 0
  calc { … } x > 0
  L(x); f(x) (lemma call)

• Types

  int bool real nat char string
  bv16 array<int> array3<int>
  set iset multiset seq map imap

• Function types:

  int->int int—->int int~>int
  (int, real, nat) tuple type
  newtype
  datatype
  class
  trait
  iterator

1.3 Declarations & Specifications🔗

requires

method Rot90(p: Point) returns (q: Point)
requires p != null
{ q := new Point; q.x, q.y := -p.y, p.x; }

ensures

method max(a: nat, b: nat) returns (m: nat)
ensures m >= a /* can have as many */
ensures m >= b /* as you like */
{ if a > b { m := a; } else { m := b; } }

assert
assume

assume x > 1;
assert 2 * x + x / x > 3;

! && || 
==> <==
<==>

assume (z || !z) && x > y;
assert j < a.Length ==> a[j]*a[j] >= 0;
assert !(a && b) <==> !a || !b;

forall
exists

assume forall n: nat :: n >= 0;
assert forall k :: k + 1 > k; /* inferred k:int */

function
predicate

function min(a: nat, b: nat): nat{
  /* body must be an expression */
  if a < b then a else b
}
predicate win(a: array<int>, j: int)
requires a != null
{ /* just like function(...): bool */
  0 <= j < a.Length
}

modifies

method Reverse(a: array<int>) /* not allowed to */
modifies a /* assign to “a” otherwise */

reads

predicate Sorted(a: array<int>) /* not allowed to */
reads a /* refer to “a[_]” otherwise */

invariant

i := 0;
while i < a.Length
invariant 0 <= i <= a.Length
invariant forall k :: 0 <= k < i ==> a[k] == 0
{ a[i], i := 0, i + 1; }
assert forall k :: 0 <= k < a.Length ==> a[k] == 0;

set
seq
multiset

var s: set<int> := {4, 2};
assert 2 in s && 3 !in s;
var q: seq<int> := [1, 4, 9, 16, 25];
assert q[2] + q[3] == q[4];
assert forall k :: k in s ==> k*k in q[1..];
var t: multiset<bool> := multiset{true, true};
assert t - multiset{true} != multiset{};

1.4 Imperative🔗

var

var n: int; 
var m := 5; /* inferred type */ 
var i: int, j: nat; 
var x, y, z: bool := 1, 2, true;

z := false;
x, y := x+y, x-y; /* parallel assignment */

if..else

if z { x := x + 1; } /* braces are */
else { y := y - 1; } /* mandatory */

if..then ..else

m := if x < y then x else y;

while forall

while x > y { x := x - y; }
forall i | 0 <= i < m { Foo(i); }

method returns

/* Without a return value */
method Hello() { print “Hello Dafny”; }
/* With a return value */
method Norm2(x: real, y: real)
returns (z: real) /* return values */
{ /* must be named */
z := x * x + y * y;
}
/* Multiple return values */
method Prod(x: int) returns (dbl: int, trpl: int)
{ dbl, trpl := x * 2, x * 3; }

class

class Point /* classes contain */
{ /* variables and methods */
var x: real, y: real
method Dist2(that: Point) returns (z: real)
requires that != null
{ z := Norm2(x - that.x, y - that.y); }
}

array

var a := new bool[2];
a[0], a[1] := true, false;
method Find(a: array<int>, v: int)
returns (index: int)