--- layout: fc_discuss_archives title: Message 41 from Frama-C-discuss on December 2011 ---
of weak invariant seems to me quite important. One can avoid a lot of redundancy when specifying the formal properties (no need to add them to each pre- and post-conditions) and make the annotations lighter (so easier to review and check for correctness). Moreover, for safety critical programs, safety properties are mapping quite well to weak invariants. Of course, I'm biased by B Method where the invariant is at the core of the correctness of the approach. That's said, I understand that the verification of invariants on complex languages like C or Ada is not that easy, as underlined by Claude and the papers he pointed. However I think that safety critical programmers can cope with restrictions, at least in a first step. After all, a safety critical program is already seriously restricted! And I'm not even talking of B Method where your program design is dictated by B's architectural restrictions. :-) Best regards, david