--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on January 2009 ---
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