--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on January 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] axiomatic definition with two indices



Hello and  thank you very much for your help.

But I would like to know, how you realized this. Is there a guideline or a
sheme which would help me to think of that on my own?
Or is it a matter of experience?

By the way, my alt-ergo (latest Lithium release) cannot proof the assertion 
either.


Cheers
 Christoph

----- Original Message ----- 
From: "Virgile Prevosto" <virgile.prevosto at cea.fr>
To: <frama-c-discuss at lists.gforge.inria.fr>
Sent: Friday, January 09, 2009 3:20 PM
Subject: Re: [Frama-c-discuss] axiomatic definition with two indices


> Hallo Christoph,
>
> Le jeu 08 jan 2009 13:03:47 CET,
> "Christoph Weber" <Christoph.Weber at first.fraunhofer.de> a ?crit :
>
>>  /*@ axiomatic Predicate_remove_copy {
>>
>>         logic integer predicate_remove_copy{La,Lb}(int* a, int* b,
>> integer i_a, integer i_b, int value);
>>        }
>>     */
>>     int remove_copy_array (int* a, int length, int* dest, int value )
>> {
>>     int i_a = 0;
>>     int i_dest = 0;
>>
>>
>>     /*@
>>     loop invariant i_dest == predicate_remove_copy{Pre,Here}(a, dest,
>> i_a-1, i_dest-1, value);
>>     */
>>     for ( ; i_a != length; ++i_a)
>>         if (a[i_a] != value)
>>         {
>>             dest[i_dest] = a[i_a];
>>             ++i_dest;
>>         }
>
> I guess that your issue stems from the fact that your axioms defining
> predicate_remove_copy (by the way it is rather a function than a
> predicate) always compare the value of predicate_remove_copy on the
> same two states La and Lb. I'd say that you need at least one axiom
> saying that if the values contained in b in states Lb1 and Lb2 are the
> same, then predicate_remove_copy returns the same result, i.e.
>
> axiom predicate_remove_copy_label{La,Lb1,Lb2}:
>         \forall int* a, int* b, value, integer i_a, i_b;
>         (\forall integer i; 0<= i <= i_b ==>
>            \at(b[i],Lb1) == \at(b[i],Lb2)) ==>
>         predicate_remove_copy{La,Lb1}(a,b,i_a,i_b,value) ==
>         predicate_remove_copy{La,Lb2}(a,b,i_a,i_b,value);
>
> In addition, adding an assertion in the loop after the update of
> dest[i_dest] seems to help the provers figuring out which instances of
> predicate_remove_copy need to be considered:
>
> /*@assert
> i_dest+1==predicate_remove_copy{Pre,Here}(a,dest,i_a,i_dest,value);
> */
>
> With these two additions, all goals are proved by alt-ergo and Z3 (but
> Simplify fails to prove the assertion)
> -- 
> E tutto per oggi, a la prossima volta.
> Virgile
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss