Verifying loops – part 2
Last time I showed how it was possible to analyse a loopfree and recursionfree program or function to determine its semantics (i.e. its weakest precondition and its postcondition), but that this didn’t work when we have loops. To make it possible to analyze loops thoroughly, ArC (along with other formal systems) requires you to provide loop invariants.
What exactly is a loop invariant? Well, it’s a Boolean expression that depends on all the variables modified by the loop, and is true when the loop is first entered, during each iteration of the loop, and when the loop terminates. Typically, it comprises two parts.
The most important part of the loop invariant is a generalization of the state that the loop is intended to achieve. It needs to be written so that it is easy to establish by suitable initialization of variables, yet it becomes exactly the desired state when the loop terminates. I’ll refer to the desired state when the loop terminates as the loop postcondition.
Let’s take a simple example. Suppose we have an array a of integers, and we want to set every element in that array to k. Here’s a function to do that:
void setArray(int * array a, size_t size, int k) pre(a.lwb == 0) pre(a.lim == size) post(forall j in 0..(size  1) : a[j] == k) { size_t i; for (i = 0; i != size; ++i) { a[i] = k; } }
The first precondition says that a is a regular pointer to the start of an array. The second one says that the number of elements is given by size. The postcondition says that when the function returns, for all indices j in the range 0 to (size – 1), a[j] is equal to k.
In this case, the loop comprises the entire body of the function, so the loop postcondition is the same as the function postcondition. In fact, loop postconditions are very frequently forall expressions, especially for loops that iterate over an array.
We need to generalise the forall expression in the postcondition so that it is true at the start of every iteration of the loop. What is the state when we are about to commence the ith iteration? Well, at that point we’ve already set all elements from zero to i1 inclusive to k, but not the elements from i onwards. We can express this with a slight modification to the forall expression:
forall j in 0..(i  1) : a[j] == k)
Do you see what I’ve done? I’ve changed the upper bound of the forall from (size – 1) to (i – 1). This gives us exactly what we need for the loop invariant:
 The loop initialisation sets i to zero, so the initial bounds of the forall are 0 .. 1 (that is, from zero up to minus one). This is an empty range (because 1 is less than 0), and a forall over an empty range is true. So the loop invariant is established at the start of the first iteration.
 During each iteration, we set the ith element to k and we increment i. So the invariant is preserved. For example, after the first iteration, the forall has range 0..0 so it just tells us that a[0] == k, which is exactly right. After the second iteration, the range is 0..1 so it says that a[0] and a[1] have value k, which is again exactly right.
 The loop terminates when i == size, because I wrote the whilecondition as i != size. If we replace i by size in the invariant, we get exactly the desired postcondition.
ArC expects the loop invariant to be written between the loop header and the body, like this:
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(forall j in 0..(i  1) : a[j] == k) { a[i] = k; } }
ArC uses the keyword keep to introduce the invariant, because we’re keeping the invariant true.
Is this enough to allow ArC to verify the loop? Unfortunately not. Using the above, ArC reports that it is unable to prove that a[j] is inbounds in the loop invariant, or that a[i] is inbounds in the loop body. So we need another component of the loop invariant, to ensure that these accesses are always in bounds. To make sure that a[i] is in bounds, we need to constrain i to be in the range 0..(size  1) at that point. But we can’t constrain i to this range in the invariant, because when the loop terminates, i ends up with the value size, which is just outside this range (remember, the invariant has to be true not only at the start of every iteration, but also when the loop terminates). So instead we constrain i to the range 0..size. The body isn’t executed when i == size, so that constraint is sufficient to guarantee that a[i] is in bounds in the body. The program then looks like this:
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; } }
I’ve put this new keep clause before the original one. The reason is that ArC reported that it couldn’t prove that a[j] was in bounds in the original keep clause. Putting the new keep clause first allows ArC to assume that i is in 0..size in the second keep clause. That is enough for it to prove that a[j] is in bounds, because j takes values from 0 to i – 1.
Have we finished? Well, ArC is able to prove that the above function meets its specification, if the loop terminates. To prove the loop terminates, we’ll need to provide a loop variant too. I’ll introduce loop variants next time.

June 22, 2010 at 11:23Aliasing and how to control it « David Crocker's Verification Blog

July 16, 2010 at 17:31Verifying pointer arithmetic « David Crocker's Verification Blog
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
 Runtime 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)