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



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