--- layout: fc_discuss_archives title: Message 70 from Frama-C-discuss on October 2008 ---
Hi again, I wonder if it will be possible to deal with behavior in loop invariants. Following example: DESCRIPTION: Compares the elements in the range [first1,last1) with those in the range beginning at first2, and returns true if the elements in both ranges are considered equal. /*@ requires last1 > first1; requires \valid_range (first1, 0, last1-first1-1); requires \valid_range (first2, 0, last1-first1-1); behavior equal: ensures \forall integer i; 0 <= i < last1-first1 ==> first1[i] == first2[i]; behavior not_equal: ensures \exists integer i; 0 <= i < last1-first1 ==> first1[i] != first2[i]; */ bool equal_int_array ( int* first1, int* last1, int* first2 ) { while ( first1!=last1 ) { if (*first1 != *first2) return false; ++first1; ++first2; } return true; } I'd like to specify the loop invriant but i guess it wont be as easy as typing: //@ ghost int* a = first1; /*@ loop invariant a <= first1 <= last1; behavior equal: loop invariant \forall integer i; 0 <= k < first-a ==> first1[k] == first2[k]; behavior not_equal: loop invariant \exists integer i; 0 <= k < first-a ==> first1[k] != first2[k]; */ Greets Christoph -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081017/e12de634/attachment-0001.htm