--- layout: fc_discuss_archives title: Message 93 from Frama-C-discuss on December 2009 ---
> > "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. Which of the scenarios listed above is true (or anyone): - The Jessie plugin generates all the "why-files" that we find in the "why" subdir (already containing all the VCs which need to be proved, but coded in Why language), after invoking it. In a second moment, the Why VC generator "process" this files (the Why ones) discharging the verification conditions to some prover, in the appropriate language ("prover language"); - The Jessie plugin generates some kind of input (which one?) to Why, and then the Why VC generator produces, finally, the VCs in why input language, with the translation to some prover in the same way as the previous scenario. I also note that in some part of the process some "j" files (Jessie files?) are generated : - What are the moment of generation of this j-files, in the context of the scenarios above? - What are the language used in this files? It is documented? 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/20091209/77988d28/attachment-0001.htm