--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on December 2011 ---
On Wed, 2011-12-07 at 15:36 +0100, David MENTRE wrote: > * Use an "atomic update" construct to avoid check strong invariant > between the two statements. I agree this approach might open a can of > worms. :-) that's how it's done in Spec#. For your example, assuming a global invariant access_count > 3 <==> locked == 1: // access_count = 3 and locked == 0 here // strong invariant holds here expose(this) { account_count++; locked = 1; } // strong invariant holds here again In addition, calling a method of an object B, that does not know anything about the invariants of object A, might break the invariant of object A. To ensure modular verification, Spec# therefore requires that such method calls are also enclosed in an expose-block. In his most recent verifier, Dafny, Rustan Leino doesn't use ownership-based invariants anymore. -- Best regards, Boris -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20111207/4c99573c/attachment.htm>