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

[Frama-c-discuss] YASE yet another specification example :)



Hello again,

I'm trying to explore a new example combining array_cpy(int* a, int n, int* b); and fill_int_array(int* first, int* last, int value).

This one is called copy_int_array (int* first, int* last, int* result).

 DESCRIPTION:
  Copies the elements in the range [first,last) into a range beginning at result.
  Returns an iterator to the last element in the destination range.
  
 Parameters:  
  first, last:
   Pointers to the initial and final positions of the searched sequence. The range 
   used is [first,last), which contains all the elements between first and last,
   including the element pointed by first but not the element pointed by last.
  result
   Pointer to the initial position in the destination sequence. This shall 
   not point to any element in the range [first,last).
  Return value:
   A pointer to the last element of the destination sequence where elements 
   have been copied.

   CODE:

/*@ predicate disjoint_arrays(int* a, int* b, integer i) =
     \forall integer k1, k2; 
        0 <= k1 < i && 0 <= k2 < i ==> a + k1 != b + k2;
*/
/*@
 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)
{
 //@ ghost int* a = first;
 //@ ghost int* b = result;
 //@ ghost int length = last-first;

    /*@
     loop invariant a <= first <= last;
     loop invariant b <= result <= b+length;     
     loop invariant \forall integer k; 0 <= k < first-a ==> result[k] == first[k];
    */
  while (first!=last) *result++ = *first++;
  return result;
}

Up to this moment Jessie is unable to solve it entirely.

Am I missing something or is it due to my Hydrogen version.

Greets

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