--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on December 2011 ---
In short, there is no plan to support global invariants in the Jessie plugin. Supporting data invariants in their full generality, as the ACSL document proposes, is challenging because of possible uncontrolled pointer aliasing might unexpectedly break invariants. Spec# ownership, mentioned by Boris Hollas, is one possible solution that were proposed in that past. Experiments were made with Jessie but were not convincing: heavy annotation overhead, and many VCs generated not discharged by automated provers. See references below In a more pragmatic point of view, there are ways to support invariants in a not-too-complex way if we impose restrictions on the allowed invariants. Typically, one may require that invariants should not include any memory dereferencing. David, may be you could encourage progress towards the support of invariants if you can tell what kind of invariants you have in mind, and in particular whether the restriction above would be too much for you or not. - Claude Asma Tafat, Sylvain Boulm?, and Claude March?. A refinement methodology for object-oriented programs. In Bernhard Beckert and Claude March?, editors, Formal Verification of Object-Oriented Software, Revised Selected Papers Presented at the International Conference, FoVeOOS 2010, volume 6528 of Lecture Notes in Computer Science, pages 153-167. Springer, January 2011. Romain Bardou. Verification of Pointer Programs Using Regions and Permissions. Th?se de doctorat, Universit? Paris-Sud, 2011. http://romain.bardou.fr/thesis/bardou11phd.pdf. Romain Bardou. Invariants de classe et syst?mes d'ownership. Master's thesis, Master Parisien de Recherche en Informatique, 2007. (in french) http://romain.bardou.fr/papers/stage2007r.pdf