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] RE : E-ACSL v0.3

  • Subject: [Frama-c-discuss] RE : E-ACSL v0.3
  • From: julien.signoles at cea.fr (SIGNOLES Julien)
  • Date: Tue, 24 Sep 2013 19:54:38 +0000
  • In-reply-to: <CAC3Lx=Z84xS_gadgAkVYhy_xbeDF_KV-P-2JSkrCeUFjnQpR-g@mail.gmail.com>
  • References: <524082A7.8080202@cea.fr>, <CAC3Lx=Z84xS_gadgAkVYhy_xbeDF_KV-P-2JSkrCeUFjnQpR-g@mail.gmail.com>
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