--- layout: post author: Virgile Prevosto date: 2010-10-06 15:51 +0200 categories: ACSL format: xhtml title: "Specification of loop assigns" summary:
ACSL's assigns
and loop assigns
clauses are a quick way to specify the intended effects of a given piece of code. However, the semantics of loop assigns
might sometimes be a bit difficult to grasp. This post tries to clarify the situation.
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
.
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
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.
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.
{% endraw %}