--- layout: fc_discuss_archives title: Message 52 from Frama-C-discuss on November 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] type invariants




Virgile Prevosto wrote:
> Hallo Christoph,
> 
> Le mar 18 nov 2008 09:14:03 CET,
> "Christoph Weber" <Christoph.Weber@first.fraunhofer.de> a ?crit :
> 
>> void out_char(char c) 
>> {
>> int col = 0;
>> //@ global invariant I : 0 <= col <= 79;
>> col++;
>> if (col >= 80) col = 0;
>> }
> 
> There is indeed a mistake in acsl-implementation.pdf. In the current
> implementation, global invariants can only be specified as global
> specification, not inside a block of code. In addition, such a global
> invariant could only refer to local variables that are static(1), as is
> the case in the example 2.42, but not in the code above. There would be
> little point in stating a "global invariant" that would depend on local
> variables whose existence is limited to a function execution
> (especially for a weak global invariant which is checked only at the
> entrance and exit of functions). There is currently no way to express
> an invariant on local variables that has to be verified at each point
> statement (short of writing assert annotations everywhere).

Not quite true:

//@ strong invariant ....

is supposed to have this semantics. But it isn't implemented yet...

> Anyway, thanks for your feedback. I hope that the situation is a bit
> clearer now.
> 
> Regards,

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |