From: "Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>
Subject: SPARK : surprising failure with implication
Date: Tue, 01 Jun 2010 20:51:04 +0200
Date: 2010-06-01T20:51:04+02:00 [thread overview]
Message-ID: <op.vdmxbejnule2fv@garhos> (raw)
Hi all,
In an Ada/SPARK source, I had something like this:
--# check (Source = 1) -> ((Source mod 2) = 1); -- (1)
--# check (Source mod 2) /= 1; -- (2)
--# check Source /= 1; -- (3)
1) Was proved by the simplifier (note that I needed a user rule for that).
2) Is a valid hypothesis ; an already proved conclusion (in some prior
check clauses)
3) Failed to be proved, while I expected this to be proved from (1) and
(2).
Naively, I had though Simplifier was not handling “(Source mod 2) /= 1” as
an equivalent of “not ((Source mod 2) = 1)”, so I tried this:
--# check (Source = 1) -> ((Source mod 2) = 1); -- (1)
--# check not ((Source mod 2) = 1); -- (2)
--# check not (Source = 1); -- (3)
Hem, I'm not silly (or am I?), where “A -> B” is valid, then “not B -> not
A” is valid too.
Whatever was going on, I wanted to be sure, so then tried the following:
--# check (Source = 1) -> ((Source mod 2) = 1); -- (1)
--# check (not ((Source mod 2) = 1)) -> (not (Source = 1)); -- (1-bis)
--# check not ((Source mod 2) = 1); -- (2)
--# check not (Source = 1); -- (3)
Simplifier failed on 1-bis. Ouch 8|
Do I become silly ?
I've looked in the *.SIV generated file, and it appears the simplifier
automatically turns things of the form “not (A = B)” into “A /= B)” (i.e.
“A <> B”, in an *.SIV file).
What I suspect: as Simplifier turns “not A = B” into “A /= B”, it cannot
see it as the negation of the antecedent and consequent of the implication
proved in (1), so from A -> B proved, I cannot prove not B -> not A, while
logically speaking, I know “(A -> B) <-> (not B -> not A)”. But it still
recognize “not ((Source mod 2) = 1)” as equivalent to “(Source mod 2) /=
1”, so I'm not sure about the reason why it fails. Or may be it can see it
as equivalent only when standalone and not in (1-bis) or against (1) ?
I was surprised to meet such an issue (unless I am missing some silly
things because I would perhaps be too much tired).
next reply other threads:[~2010-06-01 18:51 UTC|newest]
Thread overview: 11+ messages / expand[flat|nested] mbox.gz Atom feed top
2010-06-01 18:51 Yannick Duchêne (Hibou57) [this message]
2010-06-02 4:34 ` SPARK : surprising failure with implication Yannick Duchêne (Hibou57)
2010-06-02 7:42 ` Dmitry A. Kazakov
2010-06-02 7:56 ` Yannick Duchêne (Hibou57)
2010-06-02 8:55 ` Dmitry A. Kazakov
2010-06-02 8:59 ` Yannick Duchêne (Hibou57)
2010-06-02 8:50 ` Yannick Duchêne (Hibou57)
2010-06-03 8:54 ` Yannick Duchêne (Hibou57)
2010-06-03 9:06 ` Yannick Duchêne (Hibou57)
2010-06-03 11:19 ` Yannick Duchêne (Hibou57)
2010-06-03 16:45 ` Yannick Duchêne (Hibou57)
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox