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