Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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