Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] YASE - behavior

  • Subject: [Frama-c-discuss] YASE - behavior
  • From: yannick.moy at gmail.com (Yannick Moy)
  • Date: Fri Oct 17 10:45:00 2008
  • In-reply-to: <4FD9954E2DFC4E8CAA466949069E0EB8@AHARDPLACE>
  • References: <4FD9954E2DFC4E8CAA466949069E0EB8@AHARDPLACE>
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