--- layout: fc_discuss_archives title: Message 42 from Frama-C-discuss on December 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081215/cad2c01b/attachment.htm