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] Foudantions of Frama-C framework

Jo?o Paulo Carvalho wrote:
> I like to know if the assertions above are correct, in sense of 
> theoretical foundations and pratical aspects (concerning the 
> implementation) of the Frama-C deductive framework:
>
> "The ACSL is a language derived from Hoare Logic (with some higher 
> order extensions, like inductivity) and it's used to specify 
> properties concerning C programs."
>
Not correct for me.

ACSL is a BISL, Behavioral Interface Specification Language. It allows 
to specify expected properties of C programs. It is rderived from JML, 
itself derived form Eifeel and design-by-contracts concepts.

It does not impose anything on a particular technique to apply to verify 
the contrats.
> "Jessie plugin implements some calculus of weakest precondition 
> predicate transform also based on a deductive system derived from 
> Hoare Logic. That calculus is used to convert C code into another 
> language, also Hoare based: the Why input language. Aditionally, 
> Jessie plugin sintatically converts ACSL annotations into the same Why 
> input language."
>
Jessie plugin as a whole aims at generating a set of verifications 
conditions. If those are valid the the contrats are satisfied by the C 
code.
Internally it translates into the intermediate language Why, both code 
and annotations. The translation of the annotations is not more 
syntactic than translation of the code. Then the annotated Why code is 
passed to the Why VC generator, which implements a Dijkstra-style 
weakest precondition calculus. WP calculus is a way to "automatize Hoare 
logic.
> "The conditions specified in ACSL and the ones calculated from the C 
> code are merged together (by Jessie) into a single Why code (in Why input
I don't understand the "conditions specified in ACSL" and the "ones 
calculated from the C code". If you refer to runtime errors checks: 
there are just like assertions, automatically inserted.

> language), which in turn could be converted (by Why) to the dialect of 
> some prover, e.g. Gallina language of Coq theorem prover".
>
> 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                    |