--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on January 2011 ---
Hi all, Thanks Pascal for noticing the mistake in the pointer to the PLPV article. Coming back to the first request, Barbara wants a "specification of the semantics" of the Jessie language, and the 2 pages PLPV paper will certainly not answer to that. Given that fact that even the syntax of it evolved a lot in time, I'm afraid I cannot propose any up-to-date document. If you have a specific point in mind, please ask. - Claude On 01/18/2011 02:03 PM, Pascal Cuoq wrote: >> On Tue, 2011-01-18 at 12:49 +0000, Barbara Vieira wrote: >> >>> I'm working the Jessie plug-in from the Frama-C framework and I would like to know if somebody knows if there is any document specifying the semantics of the Jessie language. >>> > On Tue, Jan 18, 2011 at 1:56 PM, Boris Hollas > <hollas at informatik.htw-dresden.de> wrote: > >> There's no Jessie specific language. The language used by Jessie is >> ACSL, which is documented on frama-c.com. >> > Yes, there is. Jessie is an intermediate language before being a > Frama-C plug-in. > > The theoretical aspects are described here: > http://portal.acm.org/citation.cfm?doid=1292597.1292598 > (Claude, if you see this, fix your > http://www.lri.fr/~marche/biblio.html page, it sends to the wrong ACM > article). > > Pascal > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |