--- layout: fc_discuss_archives title: Message 101 from Frama-C-discuss on October 2008 ---
Hello, today I have something more complex. I tried to specify a function lexicogrphical_compare. This function shall compare two arrays, and return true if the first array is smaller than the other. First I need a conditional assignment. I did not find any other condition and even this one is not recognized. /*@ logic integer min(int a, int b) = (a < b) ? a : b; */ /*@ requires last > first; requires \valid_range (first1, 0, last1-first1-1); requires \valid_range (first2, 0, last2-first2-1); behavior is_less: assumes \result == true; ensures \exists integer k2; \forall integer k1; 0 <= k1 <= k2 < min(last1-first1, last2-first2) ==> ((first1[k2] < first2[k2]) ^^ (last1-first1 < last2-first2)) && first1[k1] <= first2[k1]; behavior is_not_less: assumes \result == false; 0 <= k1 <= k2 < min(last1-first1, last2-first2) ==> first1[k2] >= first2[k2] || first1[k1] >= first2[k1]; */ bool lexicographical_compare_int_array (int* first1, int* last1, int* first2, int* last2 ) { //@ ghost int* a = first1; //@ ghost int* b = first2; //@ ghost int length1 = last1-first1; //@ ghost int length2 = last2-first2; /*@ loop invariant a <= first1 <= last1; loop invariant first2 - b == first1 - a; loop invariant b <= first2 <= last2; loop invariant \forall integer k; 0 <= k < first1-a ==> a[k] == b[k]; */ for ( ; first1 != last1 && first2 != last2; ++first1, ++first2) { if (*first1 < *first2) return true; if (*first2 < *first1) return false; } return first1 == last1 && first2 != last2; } The Question is, what has to be done, that Jessie understands what I want to describe? And is my loop invariant strong/specific enough. Merci d'avance. Christoph -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081023/eadbfe88/attachment.html