--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on December 2009 ---
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." "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." "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 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 http://br.maisbuscados.yahoo.com -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091202/5ec2543c/attachment.htm