Dafny Cheatsheet
Imperative and OO
Keyword(s) What it does Snippet
var declares var nish: int;
variables var m := 5;
/* inferred type */
var i: int, j: nat;
var x, y, z: bool : = 1,
2, t
rue;
:= assignment z := false;
x, y := x+y, x-y; /* parallel assignment */
if..else conditional if z { x := x + 1 ; } /* braces are */
statement else { y : = y - 1 ; } /* mandatory */
if..then conditional m := if x < y then x else y
;
..else expression
while loops > y { x :
while x = x - y; }
forall forall i | 0 <= i < m { Foo(i); }
method subroutines /* Without a return value */
returns 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 object classes class P oint /* classes contain */
{ /* variables and methods */
var x: real, y: r
eal
method Dist2(that: Point) returns (z: real)
requires that != null
{ z := Norm2(x - that.x, y - that.y); }
}
array typed arrays var a := new bool[2
];
a[0], a[1] := true, false;
method Find(a: array<int>, v: int)
returns (index: i nt)
Specification
Keyword(s) What it does Snippet
requires precondition method Rot90(p: Point) returns (q: Point)
requires p != null
{ q := new Point; q.x, q.y := -p.y, p.x; }
ensures postcondition method max(a: nat, b: n at) r
eturns (m: n at)
ensures m >= a /* can have as many */
ensures m >= b /* as you like */
{ if a > b { m : = a; } e lse { m := b; } }
assert inline > 1;
assume x
assume propositions assert 2 * x + x / x > 3;
! && || logical assume ( z || !z) && x > y;
==> <== connectives assert j < a.Length ==> a[j]*a[j] >= 0;
<==> assert !(a && b) <==> !a || !b;
forall logical assume forall n: nat :
: n >= 0;
exists quantifiers assert forall k :: k + 1 > k; /* inferred k:int */
function pure definitions function min(a: nat, b: nat): nat
predicate { /* 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 framing (for method Reverse(a: array<int>) /* not allowed to */
methods) modifies a /* assign to “a” otherwise */
reads framing (for predicate Sorted(a: array<i
nt>) /* not allowed to */
functions) reads a /* refer to “a[_]” otherwise */
invariant loop invariants 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 standard data var s: set<int> := {4, 2
};
seq types assert 2 in s && 3 !in s;
multiset 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{};
/* more at: */
/* http://rise4fun.com/Dafny/tutorial/Collections */
