--- layout: fc_discuss_archives title: Message 101 from Frama-C-discuss on October 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] YASE lexicogrphical_compare



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