--- layout: fc_discuss_archives title: Message 41 from Frama-C-discuss on December 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

No subject



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