Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] YASE lexicogrphical_compare

  • Subject: [Frama-c-discuss] YASE lexicogrphical_compare
  • From: Christoph.Weber at first.fraunhofer.de (Christoph Weber)
  • Date: Thu Oct 23 08:25:10 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