--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on December 2011 ---
Hello Boris, 2011/12/7 Boris Hollas <hollas at informatik.htw-dresden.de> > As far as I know, different concepts for invariants are being investigated. Which kind of concepts? > The workaround I use is to define a predicate for the invariant, to #define this as pre- and postcondition and include it in the contract of each function. > However, you might write a parser or even a plugin that introduces these annotations automatically (similar to Havoc). OK, thank you for the feedback and suggestion. Best regards, david