--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on January 2009 ---
hello, I would like to know wether I missed something in the following algorithm because I cannot prove the assigns clause. I had this problem on the beta release before. /*@ requires 0 <= length; requires disjoint_arrays(a, dest, length); requires \valid_range (a, 0, length-1); requires \valid_range (dest, 0, length-1); assigns dest[0..length-1]; ensures \forall integer i; 0 <= i < length ==> dest[i] == \old(a[i]); */ int copy_array (int* a, int length, int* dest) { int index_a = 0; int index_dest = 0; /*@ loop invariant 0 <= index_a <= length; loop invariant index_dest == index_a; loop invariant 0 <= index_dest <= length; loop invariant \forall integer k; 0 <= k < index_a ==> \at(a[k],Pre) == dest[k]; loop assigns dest[0 .. index_a-1]; */ while (index_a != length) { dest[index_dest++] = a[index_a++]; } return index_dest; } Cheers Christoph -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090107/d8ad4419/attachment.htm