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

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