Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

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