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

[Frama-c-discuss] YASE - behavior



Hi,

You will have to wait for the next release of Frama-C to get behavior in
loops, but it already works as you say, with a slightly different syntax :

for <behavior_name> :  loop invariant <proposition> ;

I tried your example (correcting first in first1, adding ghost variable k),
and it translates into VC as expected.

Stay tuned for the next release!
Yannick

On Fri, Oct 17, 2008 at 9:18 AM, Christoph Weber <
Christoph.Weber@first.fraunhofer.de> wrote:

>  Hi again,
>
> I wonder if it will be possible to deal with behavior in loop invariants.
> Following example:
>
> DESCRIPTION:
>   Compares the elements in the range [first1,last1) with those in the range
> beginning
>   at first2, and returns true if the elements in both ranges are considered
> equal.
>
>
> /*@
>  requires last1 > first1;
>  requires \valid_range  (first1, 0, last1-first1-1);
>  requires \valid_range  (first2, 0, last1-first1-1);
>
>  behavior equal:
>   ensures  \forall integer i; 0 <= i < last1-first1 ==> first1[i] ==
> first2[i];
>  behavior not_equal:
>   ensures  \exists integer i; 0 <= i < last1-first1 ==> first1[i] !=
> first2[i];
> */
> bool equal_int_array ( int* first1, int* last1, int* first2 )
> {
>   while ( first1!=last1 )
>   {
>     if (*first1 != *first2)
>       return false;
>     ++first1; ++first2;
>   }
>   return true;
> }
>
> I'd like to specify the loop invriant but i guess it wont be as easy as
> typing:
>
> //@ ghost int* a = first1;
>
> /*@
>
> loop invariant a <= first1 <= last1;
>
> behavior equal:
>
>     loop invariant \forall integer i; 0 <= k < first-a ==> first1[k] ==
> first2[k];
>
> behavior not_equal:
>
>     loop invariant \exists integer i; 0 <= k < first-a ==> first1[k] !=
> first2[k];
>
> */
>
> Greets
>
> Christoph
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss@lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
>


-- 
Yannick
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081017/11e4a775/attachment.htm