--- layout: fc_discuss_archives title: Message 66 from Frama-C-discuss on April 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] one initialisation of loop invariant is not listed in jessie GUI, this time I am sure



Hello again,

I have solved my most recent question but I am not sure whether it is due to an inconsistency in the gui.

The function:

/*@
 requires 0 <= length;
 requires \valid_range(a, 0, length-1);
 requires \valid_range(b, 0, length-1);
  
 
 ensures \forall integer i; 0 <= i < length ==> swapped {Here, Old}(a+i, b+i);

*/
int swap_ranges_array(int* a, int length, int* b)
{
 int i = 0;
 int tmp;
 /*@
  loop invariant 0 <= i <= length;
  
  loop invariant \forall integer k;   
   0 <= k < i ==> swapped {Here, Pre}(a+k, b+k);
  loop invariant \forall integer k;   
   i <= k < length ==> 
   \at(a[k], Here) == \at(a[k], Pre)&&
   \at(b[k], Here) == \at(b[k], Pre);
 */
  for (;i != length; i++)
  {      
    /* swap(a+i, b+i);   */    
    tmp = a[i];    
    a[i] = b[i];   
    b[i] = tmp;
 }
  return i;
}

I would like to know, if 
loop invariant \forall integer k;   
   i <= k < length ==> 
   \at(a[k], Here) == \at(a[k], Pre)&&
   \at(b[k], Here) == \at(b[k], Pre);
should be initialized.

If everything is fine in spite this fact, I would be very happy.

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