--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on November 2009 ---
Jo?o Paulo Carvalho wrote: > > > > Now, why is this false hypothesis part of the context? Because all > > previous preconditions and postconditions are assumed to be true when > > proving subsequent properties. In other words, it behaves as if you had > > written: > > > > void bar() > > { > > //@ assert 0 <= -1; > > foo(-2); > > } > > But why that behaviour exists? There is some practical aspect that > motivates this "inclusion" of the previous ensures clauses (with the > proper variables substituted) in the next statements? In a theoretical point of view, this is given by the *weakest* precondition calculus, The weakest word is important here. In practice, there is no natural reason to remove information that comes from the context. Also, it has an interesting feature: identical precondition does not need to be proven twice, e.g in if (t[i] > 0) t[i] = ...; you are only asked to prove validity of access t[i] once. The only drawback in practice I can think of is that for large size programs, the context can get very large which can confuses automatic provers: see A Graph-based Strategy for the Selection of Hypotheses <https://wiki-cat.cea.fr/images/Couchot_hubert.pdf> - J.F. Couchot, T. Hubert http://www.lri.fr/~couchot/IMG/pdf_couchot_hubert.pdf Graph-based Reduction of Program Verification Conditions <https://wiki-cat.cea.fr/images/Couchot09afm.pdf> - J.-F. Couchot, A. Giorgetti, N. Stouls, Pr?sent? au workshop AFM de la conf?rence CAV'09. > > There are some Jessie parameter which prevents that kind of "inclusion"? > no. Could you explain why this behavior really annoys you ? > Att, > Jo?o Paulo Carvalho. > > > ------------------------------------------------------------------------ > Veja quais s?o os assuntos do momento no Yahoo! + Buscados: Top 10 > <http://br.rd.yahoo.com/mail/taglines/mail/*http://br.maisbuscados.yahoo.com/> > - Celebridades > <http://br.rd.yahoo.com/mail/taglines/mail/*http://br.maisbuscados.yahoo.com/celebridades/> > - M?sica > <http://br.rd.yahoo.com/mail/taglines/mail/*http://br.maisbuscados.yahoo.com/m%C3%BAsica/> > - Esportes > <http://br.rd.yahoo.com/mail/taglines/mail/*http://br.maisbuscados.yahoo.com/esportes/> > > ------------------------------------------------------------------------ > > _______________________________________________ > 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 |