Dafny

• Programming language designed for reasoning
• Language features drawn from:
  • Imperative programming: if, while, :=, class, ...
  • Functional programming: function, datatype, codatatype, ...
  • Proof authoring: Lemma, calc, refines, inductive predicate, ...

Dafny is aimed at reasoning

Dafny's Architecture

• Dafny uses Boogie as an intermediate verification language
• The generation of verification conditions occurs at the Boogie level
• The generated conditions are then checked by an external solver / theorem prover

Methods and Contracts

• Methods compute one or more values and may change state.
• Methods declared outside classes are allowed

method between (p: int, r: int) returns (q: int)
 requires r-p > 1
 ensures p < q < r
{
 q := (p+r) / 2;
}

Preconditions and Postconditions

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

Does this program meet the specification?

Try it online: https://rise4fun.com/Dafny

Preconditions and Postconditions

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

• Add pre-condition: we need to assume that $0\lt y$
• In general, there are two main causes for Dafny verification errors:
  • specifications that are inconsistent with the code
  • situations where it is not "clever" enough to prove the required properties.

Local Variables

• Local variables are declared with the var keyword, and can optionally have type declarations:
  • var x:int;
• Unlike method parameters, where types are required, Dafny can infer the types of local variables in almost all situations
  • var x := 0;
• Multiple variables can be declared at once:
  • var x:int, y:nat;
• The type of each variable must be given individually
  • This fails:    var x, y : int;

Exercise: Encode the following example in Dafny and read the error messages.

method m1() {
    var a := 0;
    a := 1;
    var a := 2;
    var b:int;
    var c;
    var d:int, e:bool := 0;
    var f, g := 0, false;
    var h, i:int;
}

Methods: Opacity

method Triple(x: int) returns (r: int)
 ensures r == 3*x
{
    var y := Double(x);
    r := y + x;
}

method Double(x:int) returns (r:int)
 ensures r == 2*x

This follows our discussion on Design by Contract.

Try it online: https://rise4fun.com/Dafny

Methods: Opacity

• Dafny "forgets" about the body of every method except the one it is currently working on.
• This helps us reason about our programs: we can analyze each method in isolation (given the annotations for the other methods).
• We don't care at all what happens inside each method when we call it, as long as it satisfies its annotations.
• This works because Dafny will prove that all the methods satisfy their annotations, and refuse to compile our code until they do.

Exercise: Write a method Max that takes two integer parameters and returns their maximum. Add appropriate annotations and make sure your code verifies.

Assertions

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

method TestAbs() {
    var v := Abs(3);
    assert 0 <= v;
}

Assertions can be introduced at any point. An assertion says that a particular expression always holds when control reaches that part of the code.

Assumptions

method Abs(x: int) returns (y: int)
 ensures 0 <= y
{
    if x < 0 {
        return -x;
    } else {
        return x;
    }
}
method TestAbs() {
    var v := Abs(3);
    assume v==3;
    assert 0 <= v;
    assert v==3;
}

Assumptions can be introduced at any point.

Functions

• Functions in Dafny define mathematical functions (no side-effects).
• Functions can be used in specifications!
• Example:

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

method m2() 
{
    assert abs(3) == 3;
}

Functions are transparent

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

method m2() 
{
    assert abs(3) == 3;
}

• Unlike methods, Dafny does not forget the body of a function when considering other functions. So it can expand the definition of abs in the above assertion and determine that the result is actually 3.

Exercise: Write a function max that returns the larger of two given integer parameters. Write a test method using an assert that tests your function.

Exercise: Change the specification of the method Max to use your new function.

Compiling Dafny Programs

We are not going into much detail for now, but it is possible to compile Dafny programs. Example:

method Main() 
{
    print("Hello World\n");
}

To verify, compile, and run the program:
dafny /compile:3 Main.dfy

Compiling Functions

• Functions are never part of the final compiled program: they are tools to help us verify our code.
• However, sometimes it is convenient to use a function in real code, so one can define a function method, which can be called from real code.
• Functions declared as function method are compiled and can be called from real code.

Exercise: Change your test method for Max to capture the value of max to a variable, and then do the checks from the exercise using the variable. Dafny will reject this program because you are calling max from real code. Fix this problem using a function method.

Exercise: Define the Fibonacci function and write a method with assertions that test your function.

The Fibonacci function is defined as:

Loop Invariants

• We are already familiar with the concept of loop invariant
• In Dafny, we use the keyword invariant to identify loop invariants:

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

Loop Invariants

• When you specify an invariant, Dafny proves two things: the invariant holds upon entering the loop, and it is preserved by the loop
  • By preserved, we mean that assuming that the invariant holds at the beginning of the loop, we must show that executing the loop body once makes the invariant hold again.
• Dafny can only know upon analyzing the loop body what the invariants say, in addition to the loop guard (the loop condition)

Exercise: Write a method Exp that takes an integer $m$, a natural $n$, and returns $m^n$. Write the specification in terms of a separate, recursive function exp.

Exercise: Consider the following function definition:

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

Turning this function into a function method would be extremely slow, as this version of calculating the Fibonacci numbers has exponential complexity.

Write a verified iterative algorithm that computes the $n^{th}$ Fibonacci number.

Proving Termination

• Because the halting problem is undecidable, termination analysis cannot be total.
• A simple, general method for constructing termination proofs involves associating a measure with each step of an algorithm. The measure is taken from a well-founded domain.
  • If the measure "decreases" in the domain along every possible step of the algorithm, it must terminate, because there are no infinite descending chains with respect to a well-founded domain.

Proving Termination

• A strict partially ordered domain is a pair $(W,\succ)$ where $W$ is a set and $\succ$ is a strict partial order relation over the set $W$
• A strict partial order relation $\succ$ satisfies for all $a$, $b$, and $c$ in $W$:
  • Irreflexivity: $a \not\succ a$
  • Transitivity: $a \succ b$ and $b \succ c$ then $a \succ c$
• A well-founded domain is a partially ordered domain that contains no infinite decreasing sequence $w_0 \succ w_1 \succ w_2 \succ \cdots$

Proving Termination

• The set of natural numbers equipped with the relation "greater than" $\gt$ is a well-founded domain.
• The set of integer numbers equipped with the relation "greater than" $\gt$ is not a well-founded domain. (Why?)
• Examples of well-founded domains:
  • The set of strings with the strict lexicographic order
  • The set of strings with the strict "superstring" relation

Proving Termination

1. Define a variant expression $v$ over a well-founded domain (e.g. $(\mathbb{N}, \gt)$)
2. Given a loop invariant $I$, prove: $$ \ht{I \wedge b \wedge v=x}{C}{x \gt v} $$ where $x$ is a fresh variable

Note: We can use integer expressions, as long as we show that they are non-negative before entering the loop body.

Proving Termination in Dafny

• Dafny proves that code terminates, i.e. does not loop forever, by using the decreases annotation.
• Dafny is usually able to guess the right annotations, but sometimes they need to be made explicit.
• There are two places Dafny proves termination: loops and recursion. Both of these situations require either an explicit annotation or a correct guess by Dafny.

while 0 < i
  invariant 0 <= i
  decreases i
{
    i := i - 1;
}

Exercise: Prove termination of the following loop:

method m1(m: int, n: int) 
requires 0 < m && 0 < n
{
    var x, y := m, n;

    while x != y
    invariant 0 < x && 0 < y
   {
      if x < y {
          y := y - x;
      } else {
          x := x - y;
      }
   }
}

Exercise: Termination annotations might be necessary when we have recursive methods or functions. Prove that the following function terminates:

function f(n: nat, m: nat): nat 
{
    if n==m then n 
    else if n<m then f(n, m-n) else f(n-m, m)
}

Arrays

• Arrays are a built-in part of Dafny. Their type is array<T>, where T is another type.
• They have similarities with arrays in mainstream languages such as Java:
  • Arrays can be null, and have a built-in length field, a.Length
  • Element access uses the standard bracket syntax and are indexed from zero: a[0], a[1], ...
• In Dafny, all array accesses must be proven to be within bounds. Because bounds checks are proven at verification time, no runtime checks need to be made.

Arrays

• Example: Searching an array for a particular key, returning the index of a place where we can find the key if it exists.
• We have two outcomes for a search:
  • If the algorithm returns an index (i.e. non-negative integer), then the key should be present at that index.
  • If the key is not in the array, then we would like the method to return a negative number. In this case, we want to say that the method did not miss an occurrence of the key; in other words, that the key is not in the array.

Exercise: Specify the first requirement of Find: if the algorithm returns an index (i.e. non-negative integer), then the key should be present at that index.

Use the following signature for your method:

method Find(a: array<int>, key: int) returns (index: int)

Exercise: Implement Find in a way that satisfies your specification.

Arrays

• To satisfy the first requirement:

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

• To satisfy the second requirement, we need to introduce quantifiers

Quantifiers

• A quantifier in Dafny most often takes the form of a forall expression, also called a universal quantifier. Example:

  forall k :: k < k + 1

• We often quantify over the elements of an array or data structure:

  forall k :: 0 <= k < a.length ==>  0 <= a[k]

• We can also write existential quantifications:

  exists k :: 0 <= k < a.length ==>  0 <= a[k]

Exercise: Use quantifiers to specify that the method Find returns a negative number whenever the searched key is not present in the array.

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

Exercise: Write a method that takes an integer array, which it requires to have at least one element, and returns an index to the maximum of the array's elements. Annotate the method with pre- and postconditions that state the intent of the method, and annotate its body with a loop invariant to verify it.

method FindMax(a: array<int>) returns (max: int)

Binary Search

• A linear search is not very efficient, especially when many queries are made of the same data. If the array is sorted, then we can use the very efficient binary search procedure to find the key.
• But in order for us to be able to prove our implementation correct, we need some way to require that the input array actually is sorted.
• We could do this directly with a quantifier inside a requires clause of our method, but a more modular way to express this is through a predicate.

Predicates

• A predicate is a function which returns a boolean
• For example, we define the sorted predicate over arrays of integers as a function that takes an array as an argument, and returns true if and only if that array is sorted in increasing order:

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

  Exercise

  Write this predicate in Dafny. Try to explain the error message that appears.

Predicates

• Dafny rejects the previous predicate, claiming that the predicate cannot read a.
• The sorted predicate is not able to access the array because the array was not included in the function's reading frame.
  • The reading frame of a function (or predicate) is all the memory locations that the function is allowed to read.
• The reason we might limit what a function can read is so that when we write to memory, we can be sure that functions that did not read that part of memory have the same value they did before. Framing is essential to making the verification process feasible.

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

Modifies Annotation

• Methods are allowed to read whatever memory they like, but they are required to list which parts of memory they modify, with a modifies annotation. Example:

   method m3(a: array<int>)
      requires 1 <= a.Length
      modifies a
  {
      a[0] := 42;
  }

• Reads and modifies are one of the tools that allow Dafny to work on one method at a time, because they restrict what would otherwise be arbitrary modifications of memory to something that Dafny can reason about.

Exercise: Write a verified implementation of binary search. Use the following signature:

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

Credits

• These slides use the framework reveal.js and were produced using vim and Ubuntu.
• Some slides and examples are based on material available online by Michael J. C. Gordon and Rustan Leino. Some material is taken from Dafny's tutorial.