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

[Frama-c-discuss] YASE - behavior



Hi again,

I wonder if it will be possible to deal with behavior in loop invariants.
Following example:

DESCRIPTION:
  Compares the elements in the range [first1,last1) with those in the range beginning
  at first2, and returns true if the elements in both ranges are considered equal.
  

/*@
 requires last1 > first1;
 requires \valid_range  (first1, 0, last1-first1-1);
 requires \valid_range  (first2, 0, last1-first1-1);
 
 behavior equal:
  ensures  \forall integer i; 0 <= i < last1-first1 ==> first1[i] == first2[i]; 
 behavior not_equal:
  ensures  \exists integer i; 0 <= i < last1-first1 ==> first1[i] != first2[i];  
*/
bool equal_int_array ( int* first1, int* last1, int* first2 )
{
  while ( first1!=last1 )
  {
    if (*first1 != *first2)
      return false;
    ++first1; ++first2;
  }
  return true;
}

I'd like to specify the loop invriant but i guess it wont be as easy as typing:
//@ ghost int* a = first1;

/*@

loop invariant a <= first1 <= last1;

behavior equal:

    loop invariant \forall integer i; 0 <= k < first-a ==> first1[k] == first2[k]; 

behavior not_equal:

    loop invariant \exists integer i; 0 <= k < first-a ==> first1[k] != first2[k];

*/


Greets

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