--- layout: fc_discuss_archives title: Message 128 from Frama-C-discuss on September 2013 ---
Hello David, There is nothing strange about the logic behind E-ACSL notation. The example 2.5 is just totally wrong and you're fully right: it must be a disjunction || instead of a conjunction &&. It will be fixed in the next release of E-ACSL. By the way, this tset notation is not yet supported by E-ACSL v0.3. Please let me know if you need it in your examples. Thanks for this report, Julien ________________________________________ De : frama-c-discuss-bounces at lists.gforge.inria.fr [frama-c-discuss-bounces at lists.gforge.inria.fr] de la part de David MENTRE [dmentre at linux-france.org] Date d'envoi : mardi 24 septembre 2013 10:13 ? : Frama-C public discussion Objet : Re: [Frama-c-discuss] E-ACSL v0.3 Hello Julien, 2013/9/23 Julien Signoles <Julien.Signoles at cea.fr>: > Enjoy this plug-in and do not hesitate to report your feedback. I just installed it but had no time to make extensive tests. At least it works as before on a simple example. :-) While skimming through the doc (e-acsl-implementation.pdf), I was surprised by the Example 2.5: """ Example 2.5 The set { x | integer x; 0 <= x <= 9 && 20 <= x <= 29 } denotes the set of all integers between 0 and 9 and between 20 and 29. """ Based on my comprehension of first order logic, I would have tell that this set is the empty set because an integer x cannot simultaneously be less than 9 AND bigger than 20. To denote the set of all integers between 0 and 9 and between 20 and 29, I would have written { x | integer x; 0 <= x <= 9 || 20 <= x <= 29 }. What is the logic behind E-ACSL notation? Best regards, david PS: At least, B Method as the same understanding as me, the two following assertions are proved. ;-) """ MACHINE predicate_test CONSTANTS x1, x2 PROPERTIES (x1 = { yy | yy : INTEGER & 0 <= yy & yy <= 9 & 20 <= yy & yy <= 29 }) & (x2 = { yy | yy : INTEGER & ((0 <= yy & yy <= 9) or (20 <= yy & yy <= 29)) }) ASSERTIONS (x1 = {}) & (x2 = 0..9 \/ 20..29) END """ _______________________________________________ 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