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



On Wed, 30 Apr 2014, Virgile Prevosto wrote:
You are absolutely right, the new specification is different, and on 
purpose. I could not prove the orignial specification because inp is 
changed during execution of foo() due to a call to a lower level function 
not visible at specification level. So it is intended.

Frank

  > Hello,
>
> 2014-04-29 21:27 GMT+02:00 Frank Dordowsky <frank at dordowsky.de>:
>
> 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
>

Frank Dordowsky
S?ntisstr. 37
81825 M?nchen
E-Mail: frank at dordowsky.de