--- layout: fc_discuss_archives title: Message 35 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 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