--- layout: fc_discuss_archives title: Message 125 from Frama-C-discuss on September 2013 ---
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 """