--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on January 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Type invariants



Hello Claude,

I'll have a look at the papers you cited. I know the problems that OO
introduces wrt type class invariants. Is it planned to introduce
ownership-based type invariants that can span over several struct types?
Eg,

typedef struc {
  int b;
} B;

typedef struc {
  int a;
  B b;
} A;
//@ type_invariant(A *this) = this->B.b == this a;

Invariants of this kind are allowed in Spec# and VCC. Major drawbacks
are that 
- the handling of type invariants is very difficult
- the whole verification language is centered around the invariant
concept, which complicates the verification even of programs that don't
use any invariants.

The workaround you proposed is the approach used in Havoc 0.1 for type
invariants. Havoc allows to specify pre- and postconditions that shall
hold for all functions that have a parameter of the specified type, or
for all locations in which a variable of the specified type is accessed.
That way, you can mimick weak or strong type invariants in the ACSL
sense.

Would it also be difficult to implement weak type invariants that are
limited to one type only, eg a range of type int that shall not exceed
its limits?
-- 
Regards,
Boris