--- layout: fc_discuss_archives title: Message 109 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



Something I forgot to mention:
Your [assumes] clauses mention variable \result. A warning is now issued
that says:
Error during analysis of annotation: \result meaningless
Indeed, [assumes] clauses are interpreted in the pre-state of the function,
where \result is indeed meaningless.
The correct way to go is to write an implication in the postcondition, as I
did in my answer.

Cheers,

Yannick

On Fri, Oct 24, 2008 at 1:38 AM, Yannick Moy <yannick.moy@gmail.com> wrote:

> 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
>



-- 
Yannick
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081024/93f33210/attachment.html