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



Hello Julien,

2011/12/7 Julien Signoles <Julien.Signoles at cea.fr>:
> Boris Hollas' workaround is correct for weak invariants but not for strong
> invariant:

Yes. Both Boris and me were think at weak invariants.

> in this last case, you have to insert a corresponding annotation
> at each sequence point of your program (see ACSL Reference Manual, Section
> 2.11).

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?

A work on B Method has shown that B's weak invariant are to weak to
ensure some security properties (see section IV.B of
http://arxiv.org/abs/0902.3861). However, without an atomic construct
to group statements, it seems to me impossible to update data
structures.

To give an example, I want to specify that a system should lock itself
whenever a count is greater than 3:
"""
int access_count = 0;
int locked = 0;
//@ strong global invariant access_count > 3 <==> locked == 1;
"""

Suppose I have at one point in my program access_count = 3 and locked
== 1. How can I update both value?
  account_count++; // <-- strong invariant is broken at that point
  locked = 1;

Several answers:
 * Don't do that! :-) For example "access_count > 3 ==> locked == 1"
could be updated with "locked = 1; access_count++;"

 * Use an "atomic update" construct to avoid check strong invariant
between the two statements. I agree this approach might open a can of
worms. :-)

Anyway, I'm just curious on how other people are using strong invariants.

Best regards,
david