Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Une nouvelle semaine avec nouveaux problèmes
  • From: Christoph.Weber at first.fraunhofer.de (Christoph Weber)
  • Date: Mon Oct 20 09:08:21 2008
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