Arrays#

This chapter covers fundamental array algorithms. Along the way, we’ll introduce some key concepts in Dafny: specifications, preconditions, postconditions, and loop invariants.

1.1 Max of Two Integers#

Let’s start with a method that returns the max of two integers:

method Max2(a: int, b: int) returns (m: int)
  ensures m == a || m == b
  ensures m >= a && m >= b
{
  if a >= b {
    m := a;
  } else {
    m := b;
  }
}

The ensures clauses are postconditions, which describe what the method guarantees about its output. Here, Max2 guarantees that m is one of the two inputs and it’s at least as large as both. We can also add preconditions using requires clauses, which describe what the method assumes about its inputs, but Max2 doesn’t need any. Together, the pre- and post-conditions form the method’s specification (or spec), which describes the overall behavior of the method while abstracting away the details of the body.

Dafny automatically verifies (or tries to verify) that the implementation satisfies the spec. For relatively simple methods, including Max2, Dafny can verify them without additional help. (In the VS Code extension, a green checkmark appears next to verified methods and a red X appears next to unverified methods.) But as we’ll see in the next section, Dafny sometimes needs some hints.

1.2 Max in Array#

Let’s find the largest element in an array:

method Max(a: array<int>) returns (m: int)
  requires a.Length > 0
  ensures m in a[..]
  ensures forall k :: 0 <= k < a.Length ==> a[k] <= m
{
  m := a[0];
  var i := 1;
  while i < a.Length
    invariant 1 <= i <= a.Length
    invariant m in a[..i]
    invariant forall k :: 0 <= k < i ==> a[k] <= m
  {
    if a[i] > m {
      m := a[i];
    }
    i := i + 1;
  }
}

The invariant clauses are loop invariants, which describe something that’s true at the start and end of every iteration. We write them to help Dafny makes progress toward verifying the method. Notice that in Max, the invariants are identical to the postconditions, but restricted to a[..i]. After the loop, i == a.Length, so the invariants become exactly the postconditions.