--- layout: fc_discuss_archives title: Message 108 from Frama-C-discuss on October 2008 ---
Hi, The current CVS (henceforth the next release) correctly treats the following valid annotated program. Please note I use only math integers in logic, it is usually easier because it removes the need for casts from C ints to math integers. /*@ @logic integer min(integer a, integer b) = @ (a < b) ? a : b; @ */ /*@ requires last1 > first1; requires \valid_range (first1, 0, last1-first1-1); requires \valid_range (first2, 0, last2-first2-1); behavior is_less: ensures \result == \true ==> \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: ensures \result == \false ==> \forall integer k2; \forall integer k1; 0 <= k1 <= k2 < min(last1-first1, last2-first2) ==> first1[k2] >= first2[k2] || first1[k1] >= first2[k1]; */ int 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 1; if (*first2 < *first1) return 0; } return first1 == last1 && first2 != last2; } At first glance, your annotations seem ok, but you should try it yourself with Frama-C next release. Guessing annotations is not very successful in general, much better to run them. HTH Yannick PS: I had problems just to have the code compile, could you make sure you do not have any errors besides an error that you want to report? Thanks. On Thu, Oct 23, 2008 at 8:25 AM, Christoph Weber < Christoph.Weber@first.fraunhofer.de> wrote: > 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 > > _______________________________________________ > 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/20081024/06eadc73/attachment-0001.htm