--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on January 2009 ---
Hello again, I would like to post a question regarding the reverse algorithm I sent before. Following combination of functions: /*@ requires \valid(a); requires \valid(b); ensures *a == \old(*b); ensures *b == \old(*a); */ void swap (int* a, int* b ) { int c = *a; *a = *b; *b = c; } /*@ requires 0 <= length; requires \valid_range (a, 0, length-1); ensures \forall integer k; 0 <= k < length ==> \old(a[k]) == a[length-1-k]; ensures \forall integer k; 0 <= k < length ==> a[k] == \old(a[length-1-k]); */ void reverse_array (int* a, int length) { int index_a = 0; int index_backwards = length; /*@ loop invariant 0 <= index_a <= index_backwards <= length; loop invariant index_a == length - index_backwards; loop invariant \forall integer k; 0 <= k < index_a ==> \at(a[k],Pre) == a[length-1-k]; loop invariant \forall integer k; 0 <= k < index_a ==> a[k] == \at(a[length-1-k],Pre); */ while ((index_a != index_backwards) && (index_a != index_backwards-1)) { index_backwards--; swap(&a[index_a], &a[index_backwards]); index_a++; } } My problem is the preservation of the rather complex loop invariant. I do not understand what the problem might be and I would appreciate any helpful hint. Cheers Christoph -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090108/28d426a2/attachment.htm