--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on January 2011 ---
On 01/11/2011 11:22 AM, Boris Hollas wrote: > 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? > To tell the complete story: indeed yes, an experimental ownership-based type invariants exists in the current Jessie. This is not secret, and indeed appears in the doc: see pragma InvariantPolicy and its parameter "ownership" (use it at your own risks!) The point is that we were not satisfied by the results, in particular because we had to adapt the approach to the burstall-bornat memory model of Jessie (which is different from the one of Spec# and VCC), which complicated too much the VCs. Also a lot of additional manual annotations were required (it seems that Spec# implements heuristics to discharge such a task more or less automatically) The current plan is to consider alternative approaches, for which we believe VCs will be simpler. But as I said before, it will not be implemented in the current Jessie/why 2.xx. > 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? > You're perfectly right. We already discussed about such an option in the "ACSL designing team". We agreed that it would be a good compromise. But I'm afraid that because of the lack of demand, this remained only a plan for the future. May be the designers of the WP plugin have plans to go further in this direction soon? - Claude -- 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 |