--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on January 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Pointer to Jessie input language semantics



A 2011/01/18, ?s 13:39, Claude Marche escreveu:

> On 01/18/2011 02:31 PM, Boris Hollas wrote:
>> On Tue, 2011-01-18 at 14:03 +0100, Pascal Cuoq wrote:
>>    
>> Yannick Moy's PhD contains a section on the Jessie language
>> http://www.lri.fr/~marche/moy09phd.pdf.
>>   

I completely forgot the Yannick thesis! Thanks Pascal ;-) 

> 
> Indeed, but be careful that this description and the current implementation
> may differ. So if it helps, that's perfect, otherwise please ask.

Claude, I think that it really helps a lot! I'll take care with the different aspects.
Anyway, I took a quick look at the Yannick thesis and as far as I understood it does not specify the semantics (neither the syntax) of the axiomatic statements, logic functions and logic variables. 
I will try to do it by myself. I'll contact you again if any doubt come up. 

Thanks for you help.
Best regards,
B?rbara Vieira 

> 
> - Claude
> 
> 
> -- 
> 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                    |
> 
> 
> 
> 
> 
> 
> 
> 
> _______________________________________________
> 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