--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on November 2010 ---
Le lun. 15 nov. 2010 17:10:41 CET, Guillaume Melquiond <guillaume.melquiond at inria.fr> a ?crit : > As a matter of fact, that's exactly the current ACSL interpretation. The > annotation above is syntactic sugar for > > Here42: > //@ assert \at(x,Here42) > \at(y,Here42); > > and it precisely states that for any program state at label Here42, the > value of variable x in that state is greater than the value of variable > y in that state. Well, if we are taking your interpretation literally, I think that the assert means rather 'any value that x can have in state Here42 is greater than any value that y can have in state Here42' which is not the same thing (assuming we got there at least twice of course) as fixing an arbitrary state Here42 and evaluating x and y in the same state -- Virgile Prevosto Ing?nieur-Chercheur, CEA, LIST Laboratoire de S?ret? des Logiciels +33/0 1 69 08 82 98