--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on December 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Status of global invariant in Jessie, WP and Value Analysis?



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>