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



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