--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on April 2009 ---
Hello, On Tue, Apr 7, 2009 at 09:33, Virgile Prevosto <virgile.prevosto at cea.fr> wrote: > Claude March? <Claude.Marche at inria.fr> a ?crit : > >> Another, probably quicker, possibility is first to try to prove >> >> //@ lemma l : 0=0; >> > > Shouldn't that be 0!=0 (or 0 == 1)? 0 == 0 is quite easy to prove. For people new to those issues like me, I would advise to read the following paper that explains all this in more details: A Few Remarks About Formal Development of Secure Systems http://arxiv.org/abs/0902.3861 (found in FoCaLize manual) Yours, d.