--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on October 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Some information on invariant needs



On 05.10.2012 16:56, David MENTRE wrote:
>> Note that type invariants work on types, not on individual variables. So you
>> can't uses them for the global variables in your examples.
>
> But the same approach could be used to annotate each function's pre
> and post-condition with the logic formula corresponding to the global
> invariant. An added condition would be to verify that the initial

That's indeed what happens, however only for the functions's formal 
parameters. This avoids unnecessary contracts. Global variables used by 
a function would have to be considered as auxiliary parameters, which 
requires more work.

I think that invariants are very useful and that weak invariants are 
easier to use than strong invariants. For the latter, see how this is 
handled in Spec# and Vcc.

-- 
Best regards,
Boris