## Verifying loops - Part 3: proving termination

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 write 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 eCv (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, eCv only allows loop variant expressions to have integer,
Boolean, or enumeration type. For integer variants, eCv 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:

voidsetArray(int*arraya, size_t size,intk)pre(a.lwb == 0)pre(a.lim == size)post(foralljin0..(i - 1) :- a[j] == k) { size_t i;for(i = 0; i != size; ++i)keep(iin0..size)keep(foralljin0..(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:

voidsetArray(int*arraya, size_t size,intk)pre(a.lwb == 0)pre(a.lim == size)post(foralljin0..(i - 1) :- a[j] == k) { size_t i;for(i = 0; i != size; ++i)keep(iin0..size)keep(foralljin0..(i - 1) :- a[j] ==k)decrease(size - i) { a[i] = k; } }

The expression *size – i* meets the needs of a loop variant in eCv 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 eCv doesn’t require that);
- It decreases on every iteration (because
*i*increases while*size*remains constant).

eCv 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 eCv
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 eCv 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.