--- layout: fc_discuss_archives title: Message 9 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,

Type invariants are not supported by Jessie for the moment. Moreover, 
the current
distributed version of jessie within Why 2.xx is in a frozen state: no 
new features will be added
anymore in it, instead there is a plan to develop a successor on top of 
the new Why3 engine whose first public release appeared last december. 
But I cannot announce any date for availability of it yet.

Indeed, there are on-going Ph.D. theses in the ProVal team of INRIA 
Saclay on the support of data invariants. If you want to know more 
details about why this support in difficult, I recommend to read the 
following paper: 
http://research.microsoft.com/en-us/um/people/leino/papers/krml161.pdf. 
Although it is centered to OO programming, most of the challenges listed 
also apply to C. I also recommend the paper
http://research.microsoft.com/en-us/um/people/leino/papers/krml209.pdf
which gives simple examples of programs for which type invariants are 
needed but are hard to handle.

Finally, notice that a standard workaround for the lack of type 
invariants is to declare the expected invariant as a predicate, and add 
this predicate wherever you want it, e.g in pre and/or post-conditions.

- Claude





On 01/10/2011 09:17 AM, Boris Hollas wrote:
> Hello,
>
> are type invariants supported by the upcoming or current releases of
> Jessie or WP? Can specifications for type invariants be used with option
> -jessie-infer-annot if APRON is used?
>
> Regards,
> Boris Hollas
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>    


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