--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on January 2011 ---
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