--- layout: fc_discuss_archives title: Message 45 from Frama-C-discuss on December 2008 ---
Hi Just have a look at De Morgan's laws. <http://www.nationmaster.com/encyclopedia/De-Morgan-dual> Patrick. > Now I realized, that if I would use && instead of ==> for the \exists > statement I get a green light. > But I have no Idea why, I would like to know the difference. > > Cheers > Christoph > > ----- Original Message ----- > *From:* Christoph Weber <mailto:Christoph.Weber at first.fraunhofer.de> > *To:* frama-c-discuss at lists.gforge.inria.fr > <mailto:frama-c-discuss at lists.gforge.inria.fr> > *Sent:* Monday, December 15, 2008 3:09 PM > *Subject:* [Frama-c-discuss] returns vs loop invariants > > Hello, > > thanks a lot for the help. > > The problem with this algorithms is caused in the behavior not_equal > > I think it is due to the implication > > ensures (\exists integer i; 0 <= i < length ==> \old(a[i]) != > \old(b[i])) ==> \result == 0; > > I think the "exists..." cannot be proven. > If I would reverse the implication its fine. > > I thought about a returns- statement in the loop, but I have no > idea how to use it or if it would work. > > I would appreciate any help to solve this problem. > > Besides, I havew realized, that if I would parenthesize "\result > == 1" Jessie would not list it at all. > > I use Lithium. > > /*@ > requires 0 <= length; > requires \valid_range (a, 0, length); > requires \valid_range (b, 0, length); > > assigns \nothing; > behavior equal: > ensures \result == 1 <==> (\forall integer i; 0 <= i < length ==> > \old(a[i]) == \old(b[i])); > behavior not_equal: > ensures \result == 0 <==> (\exists integer i; 0 <= i < length ==> > \old(a[i]) != \old(b[i])); > */ > int equal_array (int* a, int length, int* b ) > { > int index_a = 0; > int index_b = 0; > /*@ > loop invariant 0 <= index_a <= length; > loop invariant 0 <= index_b <= length; > loop invariant index_a == index_b; > loop invariant \forall integer k; 0 <= k < index_a ==> > \at(a[k],Pre) == \at(b[k],Pre); > > */ > while ( index_a != length ) > { > > if (a[index_a] != b[index_b]) > return 0; > ++index_a; > ++index_b; > > } > return 1; > } > > Cheers > > Christoph > > ------------------------------------------------------------------------ > _______________________________________________ > 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 > > ------------------------------------------------------------------------ > > _______________________________________________ > 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 -- Patrick Baudin, CEA, LIST, SOL, 91191 Gif-surYvette cedex, France. tel: +33 (0)1 6908 2072 -------------- section suivante -------------- Une pi?ce jointe HTML a ?t? enlev?e... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081215/7f7cba81/attachment-0001.htm