2010-10-06-Specification-of-loop-assigns.html

---
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 &lt; 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 &lt; 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 &lt; 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 &lt; 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 &lt; 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 &lt; 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 %}