--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on December 2011 ---
On 07/12/2011 15:36, David MENTRE wrote: > I still have questions on the practicality of strong invariants. > Besides simple typing invariant (e.g. a variable is in a certain > range), is there any practical use of a strong invariant if there is > no way to group a set of statements as an "atomic" construct? > Agreed. This idea (which is not unlike the expose method described by Boris Hollas) would be to use a ghost boolean (Yes, I know, support of ghost code should be improved too) that would control where the invariant can be broken. Your example would then become """ int access_count = 0; int locked = 0; //@ ghost _Bool inv_holds = 1; // not necessary, but will ensures that the strong invariant holds at // the boundaries of functions (i.e. it can only be broken temporarily // inside a given function). //@ global invariant inv_holds; //@ strong global invariant inv_holds ==> access_count> 3<==> locked == 1; //@ ghost inv_holds = 0; account_count++; locked = 1; //@ ghost inv_holds = 1; -- E tutto per oggi, a la prossima volta Virgile