--- layout: fc_discuss_archives title: Message 125 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[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
"""