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



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.

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.

Frank