Structuring Proofs

In classes 3 and 4 we continue to develop our system for reasoning formally about the meaning of a program — in this reading we discuss reasoning about functions that call other functions — and our facility with the tools Dafny offers to organize our reasoning into a cogent proof.

Calling a function

Let’s begin with an example we saw during class 1:

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

method Caller() {
  var t := Triple(18);
  assert t < 100;
}

Dafny proves the assertion t < 100 at the end of Caller: how has it done that? If we understand how to model a call to a function, we can apply the techniques from class 2 to calculate forward and backward predicates on the program state:

method Caller() {
  // What does this method call mean?
  // var t := Triple(18)

First, we make fresh variables for the inputs and outputs involved in the specification of Triple. These variables are only for this call to Triple, so we are not confused by other calls or by other functions that use the same names. Triple has a parameter x and returns result:

  var x' := 18;     // We know the argument value,        
  var result': int; // and we don't know the return value.

We do not (in principle) know the value of result'. But if we have already proved the correctness of Triple, we can use its specification without further proof. That means we are justified in assuming that the postcondition of Triple holds:

  assume result' == 3 * x';

This assumption is only reasonable because we have separately proved (or will prove) the correctness of Triple.

Finally, we complete the assignment to t from the original line of code:

  var t := result';

Overall, Caller now looks like this:

method Caller() {
  var x' := 18;
  var result': int;
  assume result' == 3 * x';
  var t := result';
  assert t < 100;
}

As we did in class 2, we can calculate predicates on the program state: forwards, to capture what we know to be true; and backwards, to capture what we need to be true.

In the forward direction:

method Caller_forward() {
  var x' := 18;
  assert x' == 18; // (1)

  var result': int;
  assert x' == 18; // (2)

  assume result' == 3 * x';
  assert x' == 18 && result' == 3 * x'; // (3)

  var t := result';
  assert x' == 18 && result' == 3 * x' && t == result'; // (4)

  assert t < 100;
}

1. After assignment, we know the value of x'.

2. Declaring result' does not tell us anything.

3. How should we model assume? If we are assuming result' == 3 * x', we can add it directly to what we know!

4. And after assignment, we know the value of t.

At this point, arithmetic allows us to prove the assertion t < 100.

And in the backwards direction — remember to read these assertions from bottom to top:

method Caller_backward() {
  assert forall result' :: result' == 3 * 18 ==> result' < 100; // (4)
  var x' := 18;

  assert forall result' :: result' == 3 * x' ==> result' < 100; // (3)
  var result': int;

  assert result' == 3 * x' ==> result' < 100; // (2)
  assume result' == 3 * x';

  assert result' < 100; // (1)
  var t := result';

  assert t < 100;
}

1. Before t’s assignment, we replace instances of t with result'.

2. Given our current formula (let’s call it Q), how should we model the statement assume P? Our intention is that if we assume P, then we will be able to show Q: a logical implication. Thus we now have P ==> Q as our goal.

3. How should we model a variable declaration? Since it establishes the name without providing any constraint on its value, we need to let that value range arbitrarily. This construction introduces a forall quantifier to our formula.

4. And before its assignment, we replace away x'.

Once again, arithmetic allows us to prove the universal implication forall result' :: result' == 3 * 18 ==> result' < 100.

Preconditions

We have seen that the specification of a function may include a precondition as well as a postcondition. In order to model the following code where we call the function Reciprocal…

method Reciprocal(x: real) returns (result: real)
  requires x != 0.0
  ensures result * x == 1.0
{
  result := 1.0 / x;
}

method Caller() {
  var half := Reciprocal(2.0);
  assert half == 0.5;
}

Recursion and induction

Can we extend our success at reasoning about functions to reasoning about recursive functions? Let’s use as an example this function, whose implementation produces a sequence of consecutive integers, similar to Python’s range():

method Upto(n: int) returns (result: seq<int>)
  requires n >= 0
  ensures forall i :: 0 <= i < |result|-1 ==> result[i] <= result[i+1]
{
  if n == 0 {
    return [];
  } else {
    var sofar := Upto(n-1);
    return sofar + [n-1];
  }
}

The provided postcondition says only that the returned sequence is sorted, but Dafny is not able to prove as much for the else branch.

To see why, let’s rewrite Upto according to our modeling of function calls:

method Upto_model(n: int) returns (result: seq<int>)
  requires n >= 0
  ensures forall i :: 0 <= i < |result|-1 ==> result[i] <= result[i+1]
{
  if n == 0 {
    return [];
  } else {
    // var sofar := Upto(n-1);
    // Introduce fresh variables for the inputs and outputs:
    var n' := n-1;
    var result': seq<int>;
    // Assert the precondition:
    assert n' >= 0;
    // Assume the postcondition:
    assume forall i :: 0 <= i < |result'|-1 ==> result'[i] <= result'[i+1];
    // Use the result:
    var sofar := result';
    return sofar + [n-1];
  }
}

Now we can calculate forward to find out what Dafny is missing:

method Upto_forward(n: int) returns (result: seq<int>)
  requires n >= 0
  ensures forall i :: 0 <= i < |result|-1 ==> result[i] <= result[i+1]
{
  if n == 0 {
    return [];
  } else {
    assert n > 0; // (1)

    // Introduce fresh variables:
    var n' := n-1;
    assert n > 0 && n' == n-1; // (2)

    var result': seq<int>;
    // Assert the precondition:
    assert n' >= 0;
    // Assume the postcondition:
    assume forall i :: 0 <= i < |result'|-1 ==> result'[i] <= result'[i+1];
    assert n > 0 && n' == n-1                                                  // (3)
           && forall i :: 0 <= i < |result'|-1 ==> result'[i] <= result'[i+1]; //    

    // Use the result:
    var sofar := result';
    assert n > 0 && n' == n-1                                                 //    
           && forall i :: 0 <= i < |result'|-1 ==> result'[i] <= result'[i+1] // (4)
           && sofar == result';                                               //    

    return sofar + [n-1];
  }
}

1. At this point we know n is at least zero, by the precondition; and not zero, since the if predicate was false; therefore greater than zero.

2. After assignment, we know the value of n'.

3. assume adds to our knowledge.

4. And after assignment we know the value of sofar.

At the return statement, what does the postcondition require? By substituting in “sofar + [n-1]” for result and simplifying:

assert forall i :: 0 <= i < |sofar| ==> (sofar + [n-1])[i] <= (sofar + [n-1])[i+1];

For nonempty sofar, at i == |sofar|-1 the consequence relates the last element of sofar to the value n-1:

sofar[|sofar|-1] <= n-1

But formula (4) only talks about the elements of sofar and their relationship between one another. It does not say anything about whether those elements are less-than-or-equal to n-1. We cannot prove the postcondition of Upto as it stands.

And so, faced with a statement we cannot prove, we make a counterintuitive (?) move: we try to prove a stronger statement. Why?

Perhaps you have made this move before in a proof by induction. In a proof by induction of some claim Q, we establish a base case (call it Q(0)) and then proceed to show that if we assume Q holds at one step, call it Q(n-1); then it holds at the next, Q(n). Because Q(n-1) is the assumption, called the induction hypothesis, that we rely on to prove Q(n), making Q stronger may result in a provable statement where a proof for weaker Q was not possible.

You can see that we have an analogous structure here: the postcondition of Upto(n-1) becomes an assumption about the state after we make that call in computing Upto(n) — that was formula (3) in Upto_forward.

Here is a new version of Upto with a much stronger postcondition:

method Upto(n: int) returns (result: seq<int>)
  requires n >= 0
  ensures |result| == n // (a)
  ensures forall i :: 0 <= i < |result| ==> result[i] == i // (b)
  ensures forall i :: 0 <= i < |result|-1 ==> result[i] <= result[i+1] // (c)
{
  if n == 0 {
    return [];
  } else {
    var sofar := Upto(n-1);
    return sofar + [n-1];
  }
}

We are now completely constraining (a) the length and (b) the values of result, along with (c) the original postcondition. Observe the result in reasoning forward about Upto:

method Upto_forward(n: int) returns (result: seq<int>)
  requires n >= 0
  ensures |result| == n
  ensures forall i :: 0 <= i < |result| ==> result[i] == i
  ensures forall i :: 0 <= i < |result|-1 ==> result[i] <= result[i+1]
{
  if n == 0 {
    return [];
  } else {
    assert n > 0; // (1)

    var n' := n-1;
    assert n > 0 && n' == n-1; // (2)

    var result': seq<int>;
    assert n' >= 0;
    assume |result'| == n'
           && forall i :: 0 <= i < |result'| ==> result'[i] == i
           && forall i :: 0 <= i < |result'|-1 ==> result'[i] <= result'[i+1];
    assert n > 0 && n' == n-1                                                  //    
           && |result'| == n'                                                  // (3)
           && forall i :: 0 <= i < |result'| ==> result'[i] == i               //    
           && forall i :: 0 <= i < |result'|-1 ==> result'[i] <= result'[i+1]; //    

    var sofar := result';
    assert n > 0 && n' == n-1                                                 //    
           && |result'| == n'                                                 //    
           && forall i :: 0 <= i < |result'| ==> result'[i] == i              // (4)
           && forall i :: 0 <= i < |result'|-1 ==> result'[i] <= result'[i+1] //    
           && sofar == result';                                               //    

    return sofar + [n-1];
  }
}

At step (3), the stronger postcondition of the recursive call gives us a stronger statement we can assert about result', which carries down to step (4).

To understand the postcondition at the return statement, we again need to substitute “sofar + [n-1]” for result to find this obligation:

assert |sofar|+1 == n                                                                 // (a)
       && forall i :: 0 <= i < |sofar|+1 ==> (sofar + [n-1])[i] == i                  // (b)
       && forall i :: 0 <= i < |sofar| ==> (sofar + [n-1])[i] <= (sofar + [n-1])[i+1] // (c)

We can show both (a) and (b) by reading off facts from the new formula (4). And since (b) gives us the specific value at every index in the array, the original postcondition (c) is no longer a problem.

In class 3, we will consider some further variations on the specification of Upto.

Summary

This reading built on the calculation rules introduced in class 2 to include calculation with function calls, and we saw the role of the induction hypothesis in reasoning about recursive functions. This kind of reasoning is as central to program verification as are function and method calls themselves in programming, so you’ll be practicing these mechanics in pretty much every upcoming class and problem set. Perhaps the key idea is to abstract a method by its specification (precondition and postcondition), so that at later calls, we do not revisit the method body but instead just reason from the specification.