--- layout: fc_discuss_archives title: Message 71 from Frama-C-discuss on October 2008 ---
Hi, Here is a correct loop invariant for your function: /*@ loop invariant a <= first <= last; loop invariant result - b == first - a; loop invariant b <= result <= b+length; loop invariant \forall integer k; 0 <= k < first-a ==> a[k] == b[k]; */ There were two problems with yours: 1) it was not strong enough to be inductive, because you did not relate the value of result and first during looping, this is the part [result - b == first - a] 2) there was an error in the last line, you meant to use the unmodified ghost versions of your pointers! With the Hydrogen version, I do not succeed to prove the postcondition, but with Helium it goes through with Z3. HTH, Yannick On Fri, Oct 17, 2008 at 8:54 AM, Christoph Weber < Christoph.Weber@first.fraunhofer.de> wrote: > 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 > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss@lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > > -- Yannick -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081017/75aab429/attachment.htm