Specification of loop assigns

A simple example

Broadly speaking, every location which is not mentioned in such a clause should have the same value when exiting the corresponding code as it when entering it. For instance, if we take the following declaration (extracted from ACSL by Example)

/*@ assigns \
othing; */
bool equal(const value_type* a  size_type n  const value_type* b);

we claim that a call to equal won't modify the global state of the program. Note that a complete specification of the function would need some requires clause about the validity of pointers but we'll ignore that in this post to concentrate on assigns.

Now the implementation of equal would be the following:

bool equal(const value_type* a  size_type n  const value_type* b)
{
  /*@ loop assigns i; */
  for (size_type i = 0; i < n; i++)
    if (a[i] != b[i])
      return 0;
  return 1;
}

This time we can not claim that the loop does not assign anything. More specifically it modifies the index i. Note that there is no contradiction with the fact that equal does not modify the global state of the program as i is only a local variable. One might argue that the scope of i being exactly the for loop it shouldn't be needed to have it mentioned in the loop assigns. However the ACSL manual explicitely says that in the case of a for loop loop annotations are evaluated after initialization takes place. In addition the other kind of loop annotations (loop variant and loop invariant) usually will refer to i and thus it wouldn't be coherent to have

/*@ loop assigns \
othing;
      loop variant n - i;
*/
for (size_type i = 0; i < n; i++) ...

If nothing is modified by the loop it'd be difficult for the variant to strictly decrease at each step. In other words if you have a "normal" for loop (i.e. not something like for(;;)) the index must be part of the loop assigns.

When the modified zone grows at each step

Not all loops modify only their index. Writing loop assigns for loops that modify different locations at each step is a bit trickier than the equal example. If we now look at a function which fills a block of code we would have the following prototype:

/*@ assigns a[0..n-1]; */
bool fill(value_type* a  size_type n  const value_type x);

meaning that we will modify the first n elements of the block pointed to by a.

When looking at the implementation a possible specification for the loop would be like this:

void fill(value_type* a  size_type n  value_type x) {
  /*@ loop assigns i a[0..(n-1)]; */
  for (size_type i = 0; i < n; i++)
    a[i] = x;
   return;
}

It is correct (at each loop steps the modified locations are included in the ones mentioned in the loop assigns) but this is an over-approximation. Let's see how we can refine it. The ACSL manual says that loop assigns are a special form of inductive invariants that is something which

1. must be true when entering the loop
2. if supposed to be true at the beginning of a loop step still holds at the end of the same step.

For a clause loop assigns P; this means that we have to prove that \at(P end_loop_step) contains both the sets of locations written by the current loop step and \at(P begin_loop_step) the set of locations written by the preceding steps. Coming back to our example at the end of the i-th step elements 0 to i-1 have been modified (we have already incremented i at the point where we evaluate the locations) so that the correct and minimal clause is

//@ loop assigns i a[0..(i-1)];

Note that for the code after the loop this does not change anything: when exiting the loop i is equal to n and thus we know that all elements up to n-1 may have been modified. However when proving something (e.g. a loop invariant) inside the loop the latter loop assigns says that all elements between i and n-1 are unchanged from their value at the very beginning of the loop while the former does provide any information on the values of these elements.

A little exercise

In order to keep up with the tradition of this blog here is a little exercise: what would be the most precise loop assigns of the following loop?

void fill(char* a  char x) {
  for(;*a;a++)
    *a = x;
   return;
}

Hint: although strictly speaking this is not needed ghost code might be helpful.