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: yannick.moy at gmail.com (Yannick Moy)
  • Date: Fri Oct 24 01:38:26 2008
  • In-reply-to: <AA14358DDC4843B3A1BD802EA1109A49@AHARDPLACE>
  • References: <AA14358DDC4843B3A1BD802EA1109A49@AHARDPLACE>
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