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

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