--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on December 2011 ---
Hello Julien, 2011/12/7 Julien Signoles <Julien.Signoles at cea.fr>: > Boris Hollas' workaround is correct for weak invariants but not for strong > invariant: Yes. Both Boris and me were think at weak invariants. > in this last case, you have to insert a corresponding annotation > at each sequence point of your program (see ACSL Reference Manual, Section > 2.11). I still have questions on the practicality of strong invariants. Besides simple typing invariant (e.g. a variable is in a certain range), is there any practical use of a strong invariant if there is no way to group a set of statements as an "atomic" construct? A work on B Method has shown that B's weak invariant are to weak to ensure some security properties (see section IV.B of http://arxiv.org/abs/0902.3861). However, without an atomic construct to group statements, it seems to me impossible to update data structures. To give an example, I want to specify that a system should lock itself whenever a count is greater than 3: """ int access_count = 0; int locked = 0; //@ strong global invariant access_count > 3 <==> locked == 1; """ Suppose I have at one point in my program access_count = 3 and locked == 1. How can I update both value? account_count++; // <-- strong invariant is broken at that point locked = 1; Several answers: * Don't do that! :-) For example "access_count > 3 ==> locked == 1" could be updated with "locked = 1; access_count++;" * Use an "atomic update" construct to avoid check strong invariant between the two statements. I agree this approach might open a can of worms. :-) Anyway, I'm just curious on how other people are using strong invariants. Best regards, david