Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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?

  • Subject: [Frama-c-discuss] Status of global invariant in Jessie, WP and Value Analysis?
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Wed, 7 Dec 2011 15:36:19 +0100
  • In-reply-to: <4EDF715E.5010601@cea.fr>
  • References: <CAC3Lx=aPPQOx6_pVXvyvy2qwCmzTPK8iJpk8rqR05R=Dr7AVbA@mail.gmail.com> <4EDF715E.5010601@cea.fr>
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