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] Res: Foudantions of Frama-C framework

> > "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