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

  • Subject: [Frama-c-discuss] Foudantions of Frama-C framework
  • From: joao_paulo_c at yahoo.com (João Paulo Carvalho)
  • Date: Wed, 2 Dec 2009 16:26:19 -0800 (PST)
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