## Verifying loops: 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 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:

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

### Latest posts

- Verifying the Liskov Substitution Principle in C++ code: Part 1
- Escher C Verifier released!
- Verifying programs that use function pointers
- eCv beta 1 released!
- Verifying programs that use ‘sizeof’
- ArC is now eCv!
- Dynamic Memory Allocation in Critical Embedded Systems
- Verifying pointer arithmetic
- Run-time checks: Are they worth it?
- Aliasing and how to control it
- Verifying absence of integer overflow
- Specification with Ghost Functions
- Expressing the Inexpressible
- Verifying a binary search, part 2
- Verifying a binary search

### Categories

### Pages

### Archives

- March 2015 (1)
- October 2011 (1)
- September 2011 (1)
- December 2010 (2)
- September 2010 (1)
- July 2010 (3)
- June 2010 (2)
- May 2010 (4)
- April 2010 (2)
- March 2010 (8)
- February 2010 (10)
- January 2010 (1)

Hello,

I wonder if there is an example of verifying, say, that a quicksort on array of ints terminates. Some time ago I tried to do that in a programming language but was bitten by disjointness constraints on the input array (with more care I could’ve persuaded the typechecker that types are correct, but …).

Hi Artyom, I can’t see any particular problem with verifying in eCv that the classic implementation of in-place quicksort terminates. Can you explain what disjointness constraints you were concerned about?

David,

Do you have plans to allow eCv to automatically infer the loop invariant and the loop decrement for simple loops? A recent ACM article (June 2011, Vol 64 #6) about indicates that Spec# is capable of doing this.

We intend to automatically infer the loop variant and the simpler parts of the loop invariant of a for-loop with a counter, where the counter is not modified in the loop body. Inferring the full loop invariant is a hard problem in the general case.