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



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