Quick language reference

Source: https://dafny.org/dafny/OnlineTutorial/guide.html

1. Declaring a Variable

var x: int := 5;

or even, with automatic type deduction:

var x := 5;

Multiline variables

var x, y, z: bool := 1, 2, true;

2. Methods

method Abs(x: int) returns (y: int)
{
  if x < 0 {
    return -x;
  } else {
    return x;
  }
}

2.1. Adding ensures clauses

This will formaly verify that the return value is always positive.

method Abs(x: int) returns (y: int)
  ensures 0 <= y
{
  if x < 0 {
    return -x;
  } else {
    return x;
  }
}

2.2. Multiple return values

method MultipleReturns(x: int, y: int) returns (more: int, less: int)
{
  more := x + y;
  less := x - y;
}

2.3. Adding method requisites

This will verify at compile time that y is greater than zero. And also ensure the result generates always less < x < more.

method MultipleReturns(x: int, y: int) returns (more: int, less: int)
  requires 0 < y
  ensures less < x < more
{
  more := x + y;
  less := x - y;
}

3. Functions

Unlike a method, which can have all sorts of statements in its body, a function body must consist of exactly one expression, with the correct type.

function abs(x: int): int
{
  ...
}

As our function returns an int, the expression must return an int, for example:

function abs(x: int): int
{
  if x < 0 then -x else x
}

The good use for functions is that they can be used in specifications from other functions (not calls):

function abs(x: int): int
{
  if x < 0 then -x else x
}
method m()
{
  assert abs(3) == 3;
}

One caveat of functions is that not only can they appear in annotations, they can only appear in annotations. You cannot create a variable like var a := abs(-4);.

4. Assertions

You can verify at any time that, at certain part of the code, an expression holds true.

method Testing()
{
  assert 2 < 3;
}

5. Loop invariants

while loops present a problem for Dafny. There is no way for Dafny to know in advance how many times the code will go around the loop. To make it possible for Dafny to work with loops, you need to provide loop invariants, another kind of annotation.

method m(n: nat)
{
  var i := 0;
  while i < n
    invariant 0 <= i
  {
    i := i + 1;
  }
}

Dafny proves two things: the invariant holds upon entering the loop and it is preserved by the loop.

An example to show how invariants work:

method m(n: nat)
{
  var i: int := 0;
  while i < n
    invariant 0 <= i <= n
  {
    i := i + 1;
  }
  assert i == n;
}

5.1. Ensuring loop termination

method m ()
{
  var i := 20;
  while 0 < i
    invariant 0 <= i
    decreases i
  {
    i := i - 1;
  }
}

Here Dafny has all the ingredients it needs to prove termination. The variable i gets smaller each loop iteration and is bounded below by zero.

If we need to count up instead of down:


method m()
{
  var i, n := 0, 20;
  while i < n
    invariant 0 <= i <= n
    decreases n - i
  {
    i := i + 1;
  }
}

If we need termination proof for recursive functions:

function fib(n: nat): nat
  decreases n
{
  if n == 0 then 0
  else if n == 1 then 1
  else fib(n - 1) + fib(n - 2)
}

6. Arrays

We can have arrays array<T> and nullable arrays array?<T>.

Arrays have a built-in lenght field array.Length

6.1. Arrays in methods

For example let’s write a function to find a value in an array

method Find(a: array<int>, key: int) returns (index: int)
  ensures 0 <= index ==> index < a.Length && a[index] == key
{
    ...
}

This states that, if and only if index is greater or equal than 0, then we’ll find a matching value a[index] == key with an index less than a.Length.

The implication is evaluated with short circuiting property, if the left is false then the implication is already true (not evaluated), which means “yes the function is correct, it hasn’t found a value, which was expected”.

6.2. Quantifiers

A quantifier in Dafny most often takes the form of a forall expression, also called a universal quantifier. This expression is true if some property holds for all elements of some set.

As an example:

method m()
{
  assert forall k :: k < k + 1;
}

A quantifier introduces a temporary name for each element of the set it is considering. This is called the bound variable, in this case k.

A pair of colons :: separates the bound variable and its optional type from the quantified property (which must be of type bool).

Now, applying them for arrays:

assert forall k :: 0 <= k < a.Length ==> ...a[k]...;

This first creates the bound variable k, then checks that k is a valid element for the array and if and only if the array is correct, it evaluates what you want to check regarding the array a[k]. A more specific example:

forall k :: 0 <= k < a.Length ==> a[k] != key

6.3. Example with arrays

method Find(a: array<int>, key: int) returns (index: int)
  ensures 0 <= index ==> index < a.Length && a[index] == key
  ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != key
{
  index := 0;
  while index < a.Length
    invariant 0 <= index <= a.Length
    invariant forall k :: 0 <= k < index ==> a[k] != key
  {
    if a[index] == key { return; }
    index := index + 1;
  }
  index := -1;
}

6.4. Take the slice of an array

I think it takes as a set but it’s very usefull:

method m()
{
  var s := [1, 2, 3, 4, 5];
  assert s[|s|-1] == 5; //access the last element
  assert s[|s|-1..|s|] == [5]; //slice just the last element, as a singleton
  assert s[1..] == [2, 3, 4, 5]; // everything but the first
  assert s[..|s|-1] == [1, 2, 3, 4]; // everything but the last
  assert s == s[0..] == s[..|s|] == s[0..|s|]; // the whole sequence
}

6.5. Check if a number is contained in an array

number in array
number in array[..i]
number in old(array[..i])

7. Predicates

A predicate is a function which returns a boolean. The use of predicates makes our code shorter, as we do not need to write out a long property over and over. It can also make our code easier to read by giving a common property a name.

For example if we want to ensure that an array is sorted, we could write the following code:

forall j, k :: 0 <= j < k < a.Length ==> a[j] <= a[k]

Here we use two bound variables, being always j < k so we can check that the array is always increasing (sorted).

With this in mind we can write the following predicate:

predicate sorted(a: array<int>)
  requires a != null
  read a
{
  forall j, k :: 0 <= j < k < a.Length ==> a[j] <= a[k]
}

There is no return type because predicates always return a boolean.

Now you can use the predicate as the following:

method BinarySearch(a: array<int>, value: int) returns (index: int)
  requires a != null && 0 <= a.Length && sorted(a)
  ...
{
  ...
}

8. Framing

8.1. Predicates

We have to state which variables the predicates read

predicate sorted(a: array<int>)
...
  read a
{
...
}

Without read a this won’t work.

8.2. Methods

In the case of methods we don’t need to state which variables are going to be read, only which ones are going to get modified.

This is done with a modifies predicate.