--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on November 2008 ---
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