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

[Frama-c-discuss] RE : E-ACSL v0.3



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