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