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

[Frama-c-discuss] Composition of COMPLEX Contracts



Hello again,

this time I am doing some exercises with Hydrogen.

I am using the copy algorithm to implement a rotate function:
It copies the values of the elements in the range [first,last) to the range positions 
beginning at result, but rotating the order of the elements in such a way that the 
element pointed by middle becomes the first element in the resulting range.

rotate_copy===========================

#include "copy.h"
#include "predicates.h"
/*@
requires last > middle >= first;
requires \valid_range (first, 0, last-first-1);
requires \valid_range (dest, 0, last-first-1);
requires disjoint_arrays(first, dest, last-first);


ensures \forall integer i; 0 <= i < middle-first ==> dest[i] == middle[i];
ensures \forall integer i; middle-first <= i < last-middle ==> dest[i] == first[i];
*/
int* rotate_copy (int* first, int* middle, int* last, int* dest )
{
dest = copy (middle, last, dest);
return copy (first, middle, dest);
}
=========================================
copy.h====================================
/*@
requires last > first;
requires disjoint_arrays(first, dest, last-first);
requires \valid_range (first, 0, last-first-1);
requires \valid_range (dest, 0, last-first-1);
assigns \nothing;
ensures \forall integer i; 0 <= i < last-first ==> dest[i] == first[i];
*/
int* copy (int* first, int* last, int* dest);
=========================================
copy.c====================================
#include "copy.h"
int* copy (int* first, int* last, int* dest)
{
int* it1 = first;
int* it2 = dest;
/*@
loop invariant first <= it1 <= last;
loop invariant it2 - dest == it1 - first;
loop invariant dest <= it2 <= dest + (last-first); 
loop invariant \forall integer k; 0 <= k < it1-first ==> first[k] == dest[k]; 
*/
while (it1 != last)
{
*it2++ = *it1++;
}
return it2;
}

The Problems are as followed:

The assigns clause in copy.h is nonesense but "assigns dest " will work even less. ()

with assigns \nothing i get copy.c proven but rotate_copy fails with preconditions.

My qeuestion is: What has to be added to get it through.



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