David Crocker's Verification Blog

If you’ve stuck with me so far in this mini-series on verifying loops, give yourself a pat on the back  before reading further. When it comes to formal verification of single-threaded software, loops are the most challenging constructs to verify. Writing loop invariants that are both correct and adequate takes serious thought and can be difficult. Another time, I’ll blog about how we can automate this process in simple cases; but that still leaves the difficult loop invariants to be constructed by hand.

I finished last time by saying that a loop invariant allows ArC (or Vcc, SPARK, or another formal system) to prove that a loop satisfies the desired state when it terminates – but only if it terminates. Unless the loop is the outermost forever-loop that embedded control software sometimes has, we’ll want to prove that the loop terminates as well. When I talk about proving loop termination, somebody usually tells me it is a waste of time trying, because of the famous halting problem. Let’s dispel that myth. The halting problem says that it is possible to write loops for which you can’t prove either termination or absence of termination. I’m not interested in those loops. I’m interested in proving that loops that are designed to terminate actually do terminate.

The easiest way to prove that a loop terminates is to use a loop variant. What is a loop variant? In its simplest form, it is a single expression that depends on variables changed by the loop, with the following two properties:

• Its type has a defined lower bound, a finite number of values, and a total ordering on those values;
• Its value decreases on every iteration of the loop.

If we can define such a variant then we know that the loop terminates, because from any starting value the lower bound must be reached after a finite number of iterations – after which it can’t decrease any more.

To ensure that the first of these properties is met, ArC only allows loop variant expressions to have integer, Boolean, or enumeration type. For integer variants, ArC assumes a lower bound of zero and will need to prove that such a variant is never negative. For Boolean expressions, the lower bound is false, and true is taken to be greater than false. For expressions of an enumeration type, the lower bound is the lowest enumeration constant defined for that type.

Let’s return to our example from last time:

void setArray(int * array a, size_t size, int k)
pre(a.lwb == 0)
pre(a.lim == size)
post(forall j in 0..(i - 1) :- a[j] == k)
{ size_t i;
for (i = 0; i != size; ++i)
keep(i in 0..size)
keep(forall j in 0..(i - 1) :- a[j] ==  k)
{ a[i] = k;
}
}

In order to show that this loop terminates, we need to add a loop variant in the form of a decrease clause. In this case, it is simple to insert a loop variant base on the loop counter:

void setArray(int * array a, size_t size, int k)
pre(a.lwb == 0)
pre(a.lim == size)
post(forall j in 0..(i - 1) :- a[j] == k)
{ size_t i;
for (i = 0; i != size; ++i)
keep(i in 0..size)
keep(forall j in 0..(i - 1) :- a[j] ==  k)
decrease(size - i)
{ a[i] = k;
}
}

The expression size – i meets the needs of a loop variant in ArC because:

• It has one of the allowed types (i.e. integer);
• It is always >= 0 inside the loop body (actually, it is >= 0 outside the loop body as well, although ArC doesn’t require that);
• It decreases on every iteration (because i increases while size remains constant).

ArC will try to prove that size – i is never negative, and that size – i decreases from one iteration to the next. The first of these is easily proven from the invariant i in 0..size. The second is easily proved because the loop increments i at the end of each iteration but leaves size alone.

For a for-loop whose header increments a loop counter from a starting value to a final value, we can always use a loop variant of the form final_value – loop_counter, provided the loop body doesn’t change loop_counter or final_value. So sometime in the future, we’ll automate discovery of ArC loop variants in cases like this.

For some loops, each iteration may make progress towards termination in either of two or more ways. For example, you could write a single loop that iterates over the elements of a two-dimensional array. Each iteration might move on to the next element in the current row, or advance to the next row if it has finished with the current one. In cases like this, defining a single variant expression for the loop can be awkward. So ArC allows you to provide a list of variant expressions. Each iteration of the loop must decrease at least one of its elements in the list, and may not increase an element unless an element earlier in the list decreases. So it must either decrease the first element, or keep the first element the same and decrease the second element, or keep the first two elements the same and decrease the third; and so on.