--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on December 2009 ---
Hello, Le mer. 02 d?c. 2009 16:26:19 CET, Jo?o Paulo Carvalho <joao_paulo_c at yahoo.com> a ?crit : > "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." In addition to what Boris said about ACSL vs Hoare logic, which is in my opinion, the main thing that needed clarification in your mail, there is a small very technical detail here: the Jessie plugin does not compute weakest pre-conditions in itself. It merely translates C+ACSL into the why language, and it is the Why tool which generates proof obligations. In fact, Why has two, mainly orthogonal, functionalities: weakest pre-conditions computation and multi-prover backend and the Jessie plug-in uses both. Hope this helps, -- E tutto per oggi, a la prossima volta. Virgile