Loops

Remember methods? Before we spent the past several weeks writing and proving the correctness of code organized into function definitions, we wrote a few method implementations like IndexOf and Upto. A method in Dafny is a piece of imperative code that, unlike a function, may reassign variables in the course of its computation, may be nondeterministic, and may even have side effects on shared data.

We started 6.S057 writing methods because of their familiar imperative syntax and because that same syntax is used in lemmas. Now we return to writing methods so that we can study how to prove the correctness of imperative code. Our starting point is a new (to us in Dafny) programming construct: loops.

method QuotientModulus() {
  // 191 ÷ 7 = 27 remainder 2
  var x := 0;
  var y := 191;
  while 7 <= y
    invariant 0 <= y && 7 * x + y == 191
  {
    x := ???;
    y := ???;
  }
  assert x == 191 / 7 == 27;
  assert y == 191 % 7 == 2;
}

method Check(Y: int) {
  // Unknown y!
  var x := 0;
  var y := Y;
  // No loop.
  // Execute one step:
  {
    x := ???;
    y := ???;
  }
  // Your code should be an incremental
  // update, not a jump to the solution.
  assert x < 7;
}

Loop specifications

Dafny’s reasoning about this loop is not formulated the way you might argue for its correctness in intro programming, which might go something like…

“We want to know how many 7’s go into y=191, so we increment x every time we subtract 7 from y. And as soon as we don’t have another 7 to subtract from it, y has the remainder.”

Instead, our formal reasoning is organized around:

• a specification for what the body of the loop guarantees called the loop invariant,
• and the loop guard expression that determines whether to execute another iteration of the loop.

By inspecting the code inside the loop, we also infer the set of variables that are potentially reassigned in the body, called the loop frame.

For a loop whose specification looks like this:

while 7 <= y                           // guard    
  invariant 0 <= y && 7 * x + y == 191 // invariant
{
  // x and y are in the frame
}

… we can model* its use in the QuotientModulus method like this:

method QuotientModulus() {
  var x, y := 0, 191;

  assert 0 <= y && 7 * x + y == 191;                // (1)
  x, y := *, *;                                     // (2)
  assume !(7 <= y) && (0 <= y && 7 * x + y == 191); // (3)

  assert x == 191 / 7 == 27;
  assert y == 191 % 7 == 2;
}

At the point where we reach the loop, (1) we must prove that the loop invariant is true. Subsequently, (2) we no longer know the particular values of the variables in the loop frame, but (3) we may assume the conjunction of the invariant and the negation of the guard. Notice that neither the loop body nor the idea that we run the loop body repeatedly — or that we run it at all — appear in this model!

The model assumes we will also prove the loop correct. What is the proof challenge? We need to show that if and when we execute the body of the loop when the guard and invariant are true, the body maintains the invariant:

var x, y;
assume (7 <= y) && (0 <= y && 7 * x + y == 191); // (1)      
x := x + 1;                                      // loop body
y := y - 7;                                      //          
assert 0 <= y && 7 * x + y == 191;               // (2)      

Notice again: we are reasoning about the loop body, but there is no repetition involved! We (1) assume the guard and invariant are true and then (2) must prove that the invariant is still true after executing the body.

We can reason backward to show our loop body is correct — remember to read these assertions from bottom to top:

assume (7 <= y) && (0 <= y && 7 * x + y == 191);

assert 0 <= y - 7 && 7 * (x + 1) + (y - 7) == 191; // (3)
x := x + 1;

assert 0 <= y - 7 && 7 * x + (y - 7) == 191; // (2)
y := y - 7;

assert 0 <= y && 7 * x + y == 191; // (1)

1. Starting from the loop invariant we need…
2. … we replace y…
3. … then replace x. The resulting obligation is indeed covered by the guard ∧ invariant assumption.

And then we can reason backward to show QuotientModulus is correct:

method QuotientModulus_model() {
  assert 0 <= 191 && 7 * 0 + 191 == 191; // (7)
  var x, y := 0, 191;

  assert 0 <= y && 7 * x + y == 191; // (6)
  assert 0 <= y && 7 * x + y == 191;

  assert forall x, y :: || (7 <= y || y < 0 || 7 * x + y != 191) // (5)
                        || (x == 191 / 7 && y == 191 % 7);       //    

  assert forall x, y :: !(7 <= y) && (0 <= y && 7 * x + y == 191) // (4)
                        ==>  x == 191 / 7 && y == 191 % 7;        //    
  x, y := *, *;

  assert !(7 <= y) && (0 <= y && 7 * x + y == 191)  ==>  x == 191 / 7 && y == 191 % 7; // (3)
  assume !(7 <= y) && (0 <= y && 7 * x + y == 191);

  assert x == 191 / 7 && y == 191 % 7; // (2)
  assert x == 191 / 7;

  assert y == 191 % 7; // (1)
  assert y == 191 % 7;
}

1. First we collect requirements from the assertions…
2. … at the end of the method.
3. Reasoning backward past the assume of ¬guard ∧ invariant, we are now trying to prove an implication.
4. We can treat the unknown new values of x and y like declarations, which introduce a forall quantifier.
5. Pausing here and rearranging the implication, we need to prove an arithmetic fact: for arbitrary x and y, either they don’t satisfy the definition of integer quotient and remainder; or, they are the correct integer quotient and remainder. This is true! You can see how we were required to show that the ¬guard ∧ invariant assumption alone was sufficient to establish further assertions about the variables that were in the loop frame.
6. Reasoning past the assert of invariant, it becomes our new obligation (in conjunction with the forall, which simplified to true, so we’ll stop writing it).
7. And finally we substitute for x and y. You can see how we are now required to show that the code before the loop establishes its invariant.

Loop termination

At the end of the day, though, a loop does loop. So after Reading 11/12 and the associated classes, you can guess that we have one more proof obligation: termination.

Dafny reasons about termination using a decreases clause that specifies the termination metric of the loop. To prove that the loop will not loop infinitely, we have another obligation in the proof of the loop body: we must show that the termination metric is smaller (in our well-founded order) after the body than it was before.

As with functions, Dafny supplies loops with a default decreases based on simple heuristics. For our example, it looks at the guard 7 <= y and derives the metric y - 7. So the proof of termination is:

var x, y;
assume (7 <= y) && (0 <= y && 7 * x + y == 191); // (1)      
ghost var d_initial := y - 7;                    // (2)      
x := x + 1;                                      // loop body
y := y - 7;                                      //          
assert d_initial > y - 7 && 0 <= y;              // (3)      

We (1) assume the guard and invariant are true, (2) notionally record the value of the termination metric, and then (3) must prove that the metric is smaller after executing the body (which in this case includes proving it hasn’t underflowed into a negative number).

Example: graph reachability

We’ll define a graph as a set of edges, where each edge is a tuple of (source node, destination node). We’ll label nodes simply with integers.

type Node = int
type Edge = (Node, Node)
type Graph = set<Edge>

The set of nodes in a graph is the set of all nodes that appear in some edge:

function Nodes(graph: Graph): set<Node> {
  (set edge | edge in graph :: edge.0) + (set edge | edge in graph :: edge.1)
}

With those definitions, here is the “agenda”-based graph-reachability procedure you saw in 6.101 translated into Dafny:

method CanReach(graph: Graph, src: Node, dst: Node) returns (b: bool)
  requires src in Nodes(graph)
{
  var frontier := {src};
  // The *frontier* holds all of the nodes that we still need to check for
  // whether they have paths to dst.
  var visited := {};
  // However, we have already processed all nodes in the *visited* set, so we
  // need not consider paths that go through this set.

  while |frontier| > 0 {
    // Pick a frontier element to work on next.
    var next :| next in frontier; // (*)
    if next == dst {
      return true; // We reached the destination!
    }
    frontier := frontier - {next};
    visited := visited + {next};
    frontier := frontier + (set e | e in graph && e.0 == next && e.1 !in visited :: e.1);
    // We expand the frontier by adding all neighbors of "next" that are not
    // already visited.
  }

  return false; // Never reached the destination.
}

The method has no postcondition: formulating and proving one will be a task for class 16. But let’s start by addressing a complaint Dafny already has about this code: it cannot prove that the loop terminates.

type Node = int
type Edge = (Node, Node)
type Graph = set<Edge>

function Nodes(graph: Graph): set<Node> {
  (set edge | edge in graph :: edge.0) + (set edge | edge in graph :: edge.1)
}

method CanReach(graph: Graph, src: Node, dst: Node) returns (b: bool)
  requires src in Nodes(graph)
{
  var frontier := {src};
  var visited := {};
  while |frontier| > 0
    invariant LoopInvariant(graph, frontier, visited)
    decreases Nodes(graph) - visited
  {
    var next :| next in frontier;
    if next == dst { return true; }
    frontier := frontier - {next};
    visited := visited + {next};
    frontier := frontier + (set e | e in graph && e.0 == next && e.1 !in visited :: e.1);
  }
  return false;
}

predicate LoopInvariant(graph: Graph, frontier: set<Node>, visited: set<Node>) {
  true
}

Summary

In the end, we see that loops are handled by Dafny in a fairly similar way to recursive functions. On the one hand, both are associated with decreases clauses to prove termination, by exhibiting metrics that go down over iterations (or recursive calls). On the other hand, we tame apparent circularity of reasoning by associating the loop (function) with a good specification, and we reason about the connections between different iterations (recursive calls) only through that specification. That specification for a loop is called the loop invariant, and writing a good loop invariant requires the same open-ended creativity as strengthening an induction hypothesis in math.