--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on December 2009 ---
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 |