--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on January 2011 ---
On 01/18/2011 03:52 PM, Barbara Vieira wrote: > >> 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. > Yes, but this is supposed to be identical to the ACSL ones, so the ACSL spec lang is the reference. > I will try to do it by myself. I'll contact you again if any doubt come up. > -- 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 |