--- layout: fc_discuss_archives title: Message 79 from Frama-C-discuss on October 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Une nouvelle semaine avec nouveaux problèmes



Hi,

in anticipation of extended behavior handling I rethought my examples in Order to reach a more complete specification.

I need to know some things:

Is there, or will there be a possibility to include requirement clauses in behavior statements?

I would like to include the cases is_empty and is_not_empty. Therefore I have to extend following spec to include zero-length arrays:

/*@
 requires last > first;
 requires disjoint_arrays(first, result, last-first);
 requires \valid_range (first, 0, last-first-1);
 requires \valid_range (result, 0, last-first-1);

 ensures  \forall integer i; 0 <= i < last-first ==> result[i] == first[i];
*/
int* copy_int_array (int* first, int* last, int* result);

altered to:
/*@
 requires last >= first;
 requires disjoint_arrays(first, result, last-first);
 behavior is_empty:
     assumes last > first;
     requires \valid_range (first, 0, last-first-1);
     requires \valid_range (result, 0, last-first-1);
     assigns  first[0..last-first-1];
     ensures  \forall integer i; 0 <= i < last-first ==> result[i] == first[i];
 behavior is_not_empty:
      assumes last == first;
      assigns \nothing;

*/
int* copy_int_array (int* first, int* last, int* result);

Referring to the assigns clause:
Will assigns \nothing ensure that nothing has been altered?
And will assigns <something> ensure that nothing else has been altered?
Would using the assigns statement make the label \at(...,Pre) in a complete copy spec obsolete?

Using the assigns statement I will encounter an other problem. Following example:

/*@
 requires 0 < n;
 requires \valid_range(a, 0, n-1);
 assigns  a[0..n - 1];
 ensures  \forall integer i; 0 <= i < n ==> a[i] == 0;
*/
void array_zero(int* a, int n)
{

    /*@ 
   loop invariant 0 <= i <= n;
   loop invariant \forall integer k; 0 <= k < i ==> a[k] == 0;
   loop assigns i, a[0..i-1];
    */
    for (int i = 0; i < n; i++)
    {
        a[i] = 0;
    }
}
If I put a assings clause in the function contract and use  a loop in the function I cannot hold the postcondition. I think it might has something to to with preserving it like a loop invariant. In the 1_3 manual I discovered the loop assigns but I don't know how to use it. (what is the upper bound and will I need to use quantifiers?)

Well that's it, I guess. 

Merci d'avance

Christoph
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081020/d97746cf/attachment.htm