Conditional proof statements, and course-of-values induction

In a proof by simple induction, we use p[i-1] to prove p[i]. Often, however, it is more convenient (and also logically sound) to use ``course-of-values'' induction. This means that to prove p[i] we assume p[j] for all j < i. SMV can do this for properties p[i] that are the result of a temporal case split. For example, suppose we have some property p defined as follows:

  p : assert G r;

Suppose further that we split cases on the value of some variable v, as follows:

  forall(i in TYPE) subcase q[i] of p for v = i;

Now, q[i] stands for the property G (v = i -> r). We can now write the following proof statement:

  forall(i in TYPE) forall(j in TYPE)
    using q[j] if j < i prove q[i];

The added clause if j < i says to only use q[j] to prove q[i] if j < i. SMV recognizes that this is a well-founded induction proof. Further, it recognizes that all the cases of q[j] where j <i can be expressed as a single temporal formula:

    G (v < i -> r)

It uses this formula to prove q[i].

As an application of course-of-values induction, consider the following example (stolen from Zohar Manna): a finite collection of processes, where each process i chooses an arbitrary number n[i] at the initial time. Each process also has a flag done[i]. Process i loops through all process indices j and waits for each process j with a number n[j] < n[i] to be ``done''. When all processes with a lower number are done, it sets its own flag done[i]. We would like to prove that every process eventually sets its done flag.

To begin with, here is a model of our system of processes:

#define MAXPROC 1000
ordset INDEX 1..MAXPROC;
ordset NAT 0..;

module main(){
  n : array INDEX of NAT;
  done : array INDEX of boolean;
  count : array INDEX of INDEX;

  forall(i in INDEX){
    next(n) := n;
    init(count[i]) := 1;
    if(n[count[i]] < n[i] -> done[count[i]]){
      next(count[i]) := count[i] + 1;
      if(count[i] = MAXPROC) next(done[i]) := 1;
    }
  }

Note we have made the type INDEX of process indices a scalarset, so that we can use induction over process indices. In addition the unbounded ordset type NAT is used to represent the numbers chosen by processes. The initial value of n[i] is arbitrary, but we constrain it too keep the same value for all future time. Each process has a variable count[i], which is incremented whenever we find the process pointed to by count[i] either has a lower number, or has set its ``done'' flag. If this happens, and count[i] has reached the maximum value, we know all done flags for processes with lower numbers have been set, so we set our own done flag.

The specification for our processes is that every process eventually sets its done flag. We write this as follows:

  forall(i in INDEX)
    p[i] : assert G F done[i];

Note, we have actually written something stronger, just because SMV is particularly fond of proving G properties. To prove this property we will actually use course-of-values induction twice. The first induction is over the number n[i]. We will split cases on this value, and assume by inductive hypothesis that any process holding a lesser value eventually sets its done flag. That is enough to show that we always eventually increment count[i], but not enough to show that count[i] eventually reaches MAXPROC. To do this we need use induction over count[i]. Thus, we split cases on count[i]. We now get to assume by inductive hypothesis that the loop terminates for all greater values of count[i]. In other words, we know that we cannot keep increasing count[i] forever, since its range is finite. Here is the resulting proof:

  forall(i in INDEX) forall(j in INDEX) forall (k in NAT){
    subcase q[i][k] of p[i] for n[i] = k;
    subcase r[i][k][j] of q[i][k] for count[i] = j;
    forall(l in NAT) forall(m in INDEX){
      using q[j][l] if l < k, r[i][k][m] if m > j
      prove r[i][k][j];
    }

The property r[i][k][j] says that process i eventually terminates if its number is k and its current count is j. To prove this, we can assume that process j (the one we are currently waiting for) terminates if its number l is less than our number k. Hence, we use q[j][l] if l < k. Further, we assume that if we get to any count m that is higher than our current count j, then we must terminate. Thus we also use r[i][k][m] if m > j. To try out this proof open this file. You should find that all the cases verify in under a second. You might want to try putting a bug in the model or the proof to see what happens. For example, what would happen if we used q[j][l] if l > k instead of k < l?

This example demonstrates two fairly general techniques. One is that to prove that a loop terminates, we split cases on the index variable of the loop and we assume termination for all values greater than the current value (or lesser if the index is decreasing). Of course, we could have used simple induction to prove termination of the loop, but this technique saves us a step, and also eliminate the value i-1, which would have contributed to case explosion and state explosion.

The other general point is that when we compare two numbers (such as n[i] and n[j]) it isn't always necessary to split cases on both values. In this case, we just split cases on n[i], and then used course-of-values induction to assume our property held for all values less than n[i]. Thus, we didn't have to know the particular value of n[j]. This technique is also quite useful in avoiding case explosion, since it saves us one parameter.