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