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]

[Frama-c-discuss] Some information on invariant needs

Hello Boris,

2012/10/4 Boris Hollas <hollas at informatik.htw-dresden.de>:
> I have a plugin that adds weak type invariants as pre- and postconditions of
> all functions that have a parameter of this type.

Thank you. That's interesting.

> 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
state does verify the invariant (that could be done through call to a
dummy function at program start that does nothing except checking its
pre-condition).


However, the purpose of my email was not about how to do such
verification (even if it is interesting to know that a work around
exists). My point was about *illustrating* the need for such kind of
specification and its verification.  Claude remark in December was:
"Invariant support is complicated. What kind of invariant do you
need?". I tried to answer that question through my examples.

I think that specifying and verifying program-wide and module-wide
invariants like in B Method or Eiffel is a needed feature for formal
program development. It helps structure the development and transform
paper requirements into verifiable formula. In other words, for me
while pre and post specify module interface, invariant specify module
internal working. Invariants should be supported by tools like
Frama-C, Why3 or GNATprove.

Some readers might make me notice that one could emulate such
invariant with current tools by defining a predicate that checks the
invariant and by including it in all pre and post-conditions of the
program. It could work. But from an engineering point of view it would
not be very good. The burden would be on the programmer to include
this predicate, one would need to verify correct use for each function
definition, etc. I think computers are better than human at checking
such things. ;-)

I would be interested to know if other practitioners of formal
development think that invariants are not that useful, and why they
think so.

Best regards,
david