--- layout: fc_discuss_archives title: Message 43 from Frama-C-discuss on December 2008 ---
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 To: 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 -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081215/aa33bb06/attachment-0001.htm