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] Behavior specification with ghost variables

Hello,

2014-04-29 21:27 GMT+02:00 Frank Dordowsky <frank at dordowsky.de>:
> There is a way to use behavior specifications together with ghost variables
> by removing the assume clause and placing the assume
> expression into a condition within the ensures clause, as shown
> in the example below:
>
>
> // file: ifbvr.h
>
> //@ ghost int inp;
>
> /*@
>   @ ensures ! ((inp >= 0) && (inp < 0));
>   @ behavior Higher:
>   @  ensures inp >= 0 ==> \result == 'p';
>   @ behavior Lower:
>   @  ensures inp < 0 ==> \result == 'n';
>   @ complete behaviors;
>   @*/
> char foo ();
>
> The top ensures clause replaces the disjoint clause, i.e. it is a
> manually established disjoint. In my example it is trivial, but it may
> get very large and complicated if there are more than two behavior
> specifications.
>

Your new specification is very different from your original one:
/*@ assumes inp < 0;
       ensures \result == 'n'; */
is equivalent to
/*@ ensures \at(inp,Old) < 0 ==> \result == 'n'; */

Unless inp is not modified by the call to foo (which is not the case
here since you want inp to reflect an internal state which is modified
at each call if I recall correctly),
in the post state (the one in which the ensures clause is evaluated),
inp != \at(inp, Old).

> I also tried model variables because they are advocated in the ACSL
> specification 1.7 as means to "...provide abstract specifications to
> functions whose concrete implementation must remain private".
> Unfortunately, it seems that model variables are not yet implemented in
> Fluorine.

Yes, at the moment only model fields (for types) are implemented in
the kernel, and I'm not completely sure of their level of support in
WP and Jessie.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile