---
layout: post
author: Virgile Prevosto
date: 2010-10-06 15:51 +0200
categories: ACSL
format: xhtml
title: "Specification of loop assigns"
summary: <p>ACSL's <code>assigns</code> and <code>loop assigns</code> clauses are a quick way to specify the intended effects of a given piece of code. However, the semantics of <code>loop assigns</code> might sometimes be a bit difficult to grasp. This post tries to clarify the situation.</p>
---
{% raw %}
<h2>A simple example</h2>
<p>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 <a href="http://first.fraunhofer.de/owx_download/acsl-by-example-5_1_0.pdf" hreflang="en">ACSL by Example</a>)</p>
<pre>/*@ assigns \
othing; */
bool equal(const value_type* a size_type n const value_type* b);
</pre>
<p>we claim that a call to <code>equal</code> won't modify the global state of the program. Note that a complete specification of the function would need some <code>requires</code> clause about the validity of pointers but we'll ignore that in this post to concentrate on <code>assigns</code>.</p>
<p>Now the implementation of equal would be the following:</p>
<pre>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;
}
</pre>
<p>This time we can not claim that the loop does not assign anything. More specifically it modifies the index <code>i</code>. Note that there is no contradiction with the fact that <code>equal</code> does not modify the global state of the program as <code>i</code> is only a local variable. One might argue that the scope of <code>i</code> being exactly the <code>for</code> loop it shouldn't be needed to have it mentioned in the <code>loop assigns</code>. However the ACSL manual explicitely says that in the case of a <code>for</code> loop loop annotations are evaluated after initialization takes place. In addition the other kind of loop annotations (<code>loop variant</code> and <code>loop invariant</code>) usually will refer to <code>i</code> and thus it wouldn't be coherent to have</p>
<pre>/*@ loop assigns \
othing;
loop variant n - i;
*/
for (size_type i = 0; i < n; i++) ...
</pre>
<p>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" <code>for</code> loop (<em>i.e.</em> not something like <code>for(;;)</code>) the index must be part of the <code>loop assigns</code>.</p>
<h2>When the modified zone grows at each step</h2>
<p>Not all loops modify only their index. Writing <code>loop assigns</code> for loops that modify different locations at each step is a bit trickier than the <code>equal</code> example. If we now look at a function which fills a block of code we would have the following prototype:</p>
<pre>/*@ assigns a[0..n-1]; */
bool fill(value_type* a size_type n const value_type x);
</pre>
<p>meaning that we will modify the first <code>n</code> elements of the block pointed to by <code>a</code>.</p>
<p>When looking at the implementation a possible specification for the loop would be like this:</p>
<pre>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;
}
</pre>
<p>It is correct (at each loop steps the modified locations are included in the ones mentioned in the <code>loop assigns</code>) but this is an over-approximation. Let's see how we can refine it. The ACSL manual says that <code>loop assigns</code> are a special form of <em>inductive</em> invariants that is something which</p>
<ol>
<li>must be true when entering the loop</li>
<li>if supposed to be true at the beginning of a loop step still holds at the end of the same step.</li>
</ol>
<p>For a clause <code>loop assigns P;</code> this means that we have to prove that <code>\at(P end_loop_step)</code> contains both the sets of locations written by the current loop step and <code>\at(P begin_loop_step)</code> the set of locations written by the preceding steps. Coming back to our example at the end of the <code>i</code>-th step elements <code>0</code> to <code>i-1</code> have been modified (we have already incremented <code>i</code> at the point where we evaluate the locations) so that the correct and minimal clause is</p>
<pre>//@ loop assigns i a[0..(i-1)];
</pre>
<p>Note that for the code after the loop this does not change anything: when exiting the loop <code>i</code> is equal to <code>n</code> and thus we know that all elements up to <code>n-1</code> may have been modified. However when proving something (<em>e.g.</em> a <code>loop invariant</code>) inside the loop the latter <code>loop assigns</code> says that all elements between <code>i</code> and <code>n-1</code> 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.</p>
<h2>A little exercise</h2>
<p>In order to keep up with the tradition of this blog here is a little exercise: what would be the most precise <code>loop assigns</code> of the following loop?</p>
<pre>void fill(char* a char x) {
for(;*a;a++)
*a = x;
return;
}
</pre>
<p>Hint: although strictly speaking this is not needed ghost code might be helpful.</p>
<h2>A simple example</h2>
<p>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 <a href="http://first.fraunhofer.de/owx_download/acsl-by-example-5_1_0.pdf" hreflang="en">ACSL by Example</a>)</p>
<pre>/*@ assigns \
othing; */
bool equal(const value_type* a size_type n const value_type* b);
</pre>
<p>we claim that a call to <code>equal</code> won't modify the global state of the program. Note that a complete specification of the function would need some <code>requires</code> clause about the validity of pointers but we'll ignore that in this post to concentrate on <code>assigns</code>.</p>
<p>Now the implementation of equal would be the following:</p>
<pre>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;
}
</pre>
<p>This time we can not claim that the loop does not assign anything. More specifically it modifies the index <code>i</code>. Note that there is no contradiction with the fact that <code>equal</code> does not modify the global state of the program as <code>i</code> is only a local variable. One might argue that the scope of <code>i</code> being exactly the <code>for</code> loop it shouldn't be needed to have it mentioned in the <code>loop assigns</code>. However the ACSL manual explicitely says that in the case of a <code>for</code> loop loop annotations are evaluated after initialization takes place. In addition the other kind of loop annotations (<code>loop variant</code> and <code>loop invariant</code>) usually will refer to <code>i</code> and thus it wouldn't be coherent to have</p>
<pre>/*@ loop assigns \
othing;
loop variant n - i;
*/
for (size_type i = 0; i < n; i++) ...
</pre>
<p>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" <code>for</code> loop (<em>i.e.</em> not something like <code>for(;;)</code>) the index must be part of the <code>loop assigns</code>.</p>
<h2>When the modified zone grows at each step</h2>
<p>Not all loops modify only their index. Writing <code>loop assigns</code> for loops that modify different locations at each step is a bit trickier than the <code>equal</code> example. If we now look at a function which fills a block of code we would have the following prototype:</p>
<pre>/*@ assigns a[0..n-1]; */
bool fill(value_type* a size_type n const value_type x);
</pre>
<p>meaning that we will modify the first <code>n</code> elements of the block pointed to by <code>a</code>.</p>
<p>When looking at the implementation a possible specification for the loop would be like this:</p>
<pre>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;
}
</pre>
<p>It is correct (at each loop steps the modified locations are included in the ones mentioned in the <code>loop assigns</code>) but this is an over-approximation. Let's see how we can refine it. The ACSL manual says that <code>loop assigns</code> are a special form of <em>inductive</em> invariants that is something which</p>
<ol>
<li>must be true when entering the loop</li>
<li>if supposed to be true at the beginning of a loop step still holds at the end of the same step.</li>
</ol>
<p>For a clause <code>loop assigns P;</code> this means that we have to prove that <code>\at(P end_loop_step)</code> contains both the sets of locations written by the current loop step and <code>\at(P begin_loop_step)</code> the set of locations written by the preceding steps. Coming back to our example at the end of the <code>i</code>-th step elements <code>0</code> to <code>i-1</code> have been modified (we have already incremented <code>i</code> at the point where we evaluate the locations) so that the correct and minimal clause is</p>
<pre>//@ loop assigns i a[0..(i-1)];
</pre>
<p>Note that for the code after the loop this does not change anything: when exiting the loop <code>i</code> is equal to <code>n</code> and thus we know that all elements up to <code>n-1</code> may have been modified. However when proving something (<em>e.g.</em> a <code>loop invariant</code>) inside the loop the latter <code>loop assigns</code> says that all elements between <code>i</code> and <code>n-1</code> 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.</p>
<h2>A little exercise</h2>
<p>In order to keep up with the tradition of this blog here is a little exercise: what would be the most precise <code>loop assigns</code> of the following loop?</p>
<pre>void fill(char* a char x) {
for(;*a;a++)
*a = x;
return;
}
</pre>
<p>Hint: although strictly speaking this is not needed ghost code might be helpful.</p>
{% endraw %}