--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on November 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Res: Feature or bug?



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                    |