--- layout: fc_discuss_archives title: Message 42 from Frama-C-discuss on April 2014 ---
[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