--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on October 2012 ---
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