* SPARK : surprising failure with implication
@ 2010-06-01 18:51 Yannick Duchêne (Hibou57)
2010-06-02 4:34 ` Yannick Duchêne (Hibou57)
2010-06-02 8:50 ` Yannick Duchêne (Hibou57)
0 siblings, 2 replies; 11+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2010-06-01 18:51 UTC (permalink / 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).
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: SPARK : surprising failure with implication
2010-06-01 18:51 SPARK : surprising failure with implication Yannick Duchêne (Hibou57)
@ 2010-06-02 4:34 ` Yannick Duchêne (Hibou57)
2010-06-02 7:42 ` Dmitry A. Kazakov
2010-06-02 8:50 ` Yannick Duchêne (Hibou57)
1 sibling, 1 reply; 11+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2010-06-02 4:34 UTC (permalink / raw)
Le Tue, 01 Jun 2010 20:51:04 +0200, Yannick Duchêne (Hibou57)
<yannick_duchene@yahoo.fr> a écrit:
> 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).
>
> [...]
Although late, I'm back to this topic.
I added this user rule:
my_logic(1): not B -> not A may_be_deduced_from [ (A -> B) ].
While this was looking so much obvious, I though the Simplifier already
knew it and this would probably change nothing. But this did change
something! Now the above sequence of hypothesis->conclusion is proved.
Did I made something wrong somewhere ? Did I brake something somewhere ?
Why is not this fundamental rule embedded in the Simplifier ?
I was so much surprised, that I checked it (yes, what looks obvious is
sometimes good to check). Can't say anything else that “yes, this is true”.
(A) (B) (A->B)
F F T
F T T
T F F
T T T
(not B) (not A) (not B -> not A)
T T T
F T T
T F F
F F T
(A -> B) (not B -> not A) ((A -> B) -> (not B -> not A))
T T T
T T T
F F T
T T T
This is indeed tautology.
OK, that is solved, but I'm still somewhat frightened by what I don't
understand in this experience : why did I need to add a user rule for that
? What was wrong ?
--
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
-- i.e. forget about previous premises which leads to conclusion
-- and start with new conclusion as premise.
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: SPARK : surprising failure with implication
2010-06-02 4:34 ` Yannick Duchêne (Hibou57)
@ 2010-06-02 7:42 ` Dmitry A. Kazakov
2010-06-02 7:56 ` Yannick Duchêne (Hibou57)
0 siblings, 1 reply; 11+ messages in thread
From: Dmitry A. Kazakov @ 2010-06-02 7:42 UTC (permalink / raw)
(forall A,B in Boolean)
not B => not A =
= not not B or not A =
= B or not A =
= not A or B =
= A => B
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: SPARK : surprising failure with implication
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
0 siblings, 1 reply; 11+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2010-06-02 7:56 UTC (permalink / raw)
Le Wed, 02 Jun 2010 09:42:58 +0200, Dmitry A. Kazakov
<mailbox@dmitry-kazakov.de> a écrit:
> (forall A,B in Boolean)
>
> not B => not A =
> = not not B or not A =
> = B or not A =
> = not A or B =
> = A => B
>
Yes, you confirmed that is right and so I'm not silly. But why Simplifier
do not seems to know it ? It is the basis of inference logic. That is why
I have such a weighty question in my mind : I wonder if I did something
wrong somewhere or if something is broken.
Do you have an idea ?
--
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
-- i.e. forget about previous premises which leads to conclusion
-- and start with new conclusion as premise.
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: SPARK : surprising failure with implication
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)
0 siblings, 1 reply; 11+ messages in thread
From: Dmitry A. Kazakov @ 2010-06-02 8:55 UTC (permalink / raw)
On Wed, 02 Jun 2010 09:56:23 +0200, Yannick Duch�ne (Hibou57) wrote:
> Le Wed, 02 Jun 2010 09:42:58 +0200, Dmitry A. Kazakov
> <mailbox@dmitry-kazakov.de> a �crit:
>
>> (forall A,B in Boolean)
>>
>> not B => not A =
>> = not not B or not A =
>> = B or not A =
>> = not A or B =
>> = A => B
>>
> Yes, you confirmed that is right and so I'm not silly. But why Simplifier
> do not seems to know it ? It is the basis of inference logic.
Modus ponens is, but in the form:
A => B, A
--------------
B
You have rather unusual:
A => B, not B
--------------------
not A
Disproving the antecedent from wrong consequent is not very common.
> That is why
> I have such a weighty question in my mind : I wonder if I did something
> wrong somewhere or if something is broken.
>
> Do you have an idea ?
None, except that what looks obvious for a man is not for a computer and
conversely. (:-))
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: SPARK : surprising failure with implication
2010-06-02 8:55 ` Dmitry A. Kazakov
@ 2010-06-02 8:59 ` Yannick Duchêne (Hibou57)
0 siblings, 0 replies; 11+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2010-06-02 8:59 UTC (permalink / raw)
Le Wed, 02 Jun 2010 10:55:48 +0200, Dmitry A. Kazakov
<mailbox@dmitry-kazakov.de> a écrit:
> Disproving the antecedent from wrong consequent is not very common.
It is to me, and not only with SPARK rules, this is why I though to use it
in this context.
Thanks to have pointed this may not seems common to every one, as I was
not aware of this.
> None, except that what looks obvious for a man is not for a computer and
> conversely. (:-))
You are right Dmitry ;) That is a nice sentence in all of its
interpretations.
--
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
-- i.e. forget about previous premises which leads to conclusion
-- and start with new conclusion as premise.
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: SPARK : surprising failure with implication
2010-06-01 18:51 SPARK : surprising failure with implication Yannick Duchêne (Hibou57)
2010-06-02 4:34 ` 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 16:45 ` Yannick Duchêne (Hibou57)
1 sibling, 2 replies; 11+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2010-06-02 8:50 UTC (permalink / raw)
Not exactly with implication this time, this is about equality and
substitution.
Here is a case I am facing (simplified for the purpose of this message):
--# assert S = (I / X); -- (1)
--# check S = T'Pos (S); -- (2)
--# check I = T'Pos (I); -- (3)
--# check T'Pos (S) = (T'Pos (I) / X); -- (4)
(1) is proved
(2) and (3) are proved
Simplifier fails to prove (4) despite of (1) and equalities (2) and (3)
which should be used to substitute S and I in (1).
I still did not found a workaround for this one (I am busy at this now).
Does anyone already meet a case similar to this one ? Does it fails for
the reason it requires two substitutions at a time ?
S and I are both of type same T (which is a modular type). Anyway, this
should not be of any importance, as what is this about here, is that two
equalities are not used for a substitution where it could expected to be.
It is not possible to use an intermediate step like...
--# check S = (T'Pos (I) / X); -- (4.1)
--# check T'Pos (S) = (T'Pos (I) / X); -- (4.2)
...because on (4.1), this would be an Universal_Integer expression on the
right side with an expression of type T on the left side, which is not an
allowed ; so there is no way to avoid the need for two substitutions at a
time.
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: SPARK : surprising failure with implication
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)
1 sibling, 2 replies; 11+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2010-06-03 8:54 UTC (permalink / raw)
Le Wed, 02 Jun 2010 10:50:55 +0200, Yannick Duchêne (Hibou57)
<yannick_duchene@yahoo.fr> a écrit:
> Not exactly with implication this time, this is about equality and
> substitution.
>
> Here is a case I am facing (simplified for the purpose of this message):
>
> --# assert S = (I / X); -- (1)
> --# check S = T'Pos (S); -- (2)
> --# check I = T'Pos (I); -- (3)
> --# check T'Pos (S) = (T'Pos (I) / X); -- (4)
>
> (1) is proved
> (2) and (3) are proved
> Simplifier fails to prove (4) despite of (1) and equalities (2) and (3)
> which should be used to substitute S and I in (1).
>
> I still did not found a workaround for this one (I am busy at this now).
>
> Does anyone already meet a case similar to this one ? Does it fails for
> the reason it requires two substitutions at a time ?
A example which made me think about this one, while different. This time,
there is only one substitution, and it still fails.
First, the case (extract from an *.SIV file):
C1: instance mod 2 ** (result + 1) * 2 ** (7 - result) * 2 mod 256 =
instance mod 2 ** (result - 1 + 2) * 2 ** (7 - result) * 2
mod 256 .
And its precursor as it appears in the *.VCG file:
C1: source * 2 mod instance_type__modulus = instance mod
base ** (result - 1 + 2) * base ** (u__last - (
result - 1 + 1)) * 2 mod base ** (u__last + 1) .
This conclusion could not be proved, because it fails to simplify (result
- 1 + 2) into (result + 1), and I've checked it also fails to substitute
(result - 1 + 2) to (result + 1). I have tried many thing, including a
user rule like this one as my last attempt:
my_test(1): A - 1 + 2 may_be_replaced_by [ A + 1 ].
As well as
my_test(2): (A - 1) + 2 may_be_replaced_by [ A + 1 ].
Without success.
The original context in Ada/SPARK source is of the form (the above C1
stands for the Check clause):
--# assert ..... U'Pos (Result + 1) .....
.....
Result := Result + 1;
.....
--# check .... U'Pos (Result + 1 + 1) ....
I suspect it to see Result - 1, standing for the value of Result in the
Assert clause (and thus as the actual expression standing for Result), as
a monolithic subexpression. If this is really what happens, then it would
not see (Result + 1 + 1) as (Result - 1 + 1 + 1), and instead as ((Result
- 1) + 1 + 1), then see 1 + 1 as an expression, which is simplifies to 2,
getting ((Result - 1) + 2), which it could not simplify any more, as it
could not see -1 + 2 as a simplifiable expression, because -1 belongs to a
subexpression.
However, what it strange, it that Result - 1 does not appears as a
subexpression in neither the SIV file nor the VCG file. So I wonder if
this is really the explanation of what's going on. Further more, the two
attempt with above user rules, did not solve anything. Both simplification
of a constant expression and substitution fails here.
Probably needs even more investigation.
--
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
-- i.e. forget about previous premises which leads to conclusion
-- and start with new conclusion as premise.
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: SPARK : surprising failure with implication
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)
1 sibling, 0 replies; 11+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2010-06-03 9:06 UTC (permalink / raw)
Le Thu, 03 Jun 2010 10:54:51 +0200, Yannick Duchêne (Hibou57)
<yannick_duchene@yahoo.fr> a écrit:
> I suspect it to see Result - 1, standing for the value of Result in the
> Assert clause (and thus as the actual expression standing for Result),
> as a monolithic subexpression. If this is really what happens, then it
> would not see (Result + 1 + 1) as (Result - 1 + 1 + 1), and instead as
> ((Result - 1) + 1 + 1), then see 1 + 1 as an expression, which is
> simplifies to 2, getting ((Result - 1) + 2), which it could not simplify
> any more, as it could not see -1 + 2 as a simplifiable expression,
> because -1 belongs to a subexpression.
Note for readers : if you are not aware of how SPARK and Simplifier works,
reading “see (Result + 1 + 1) as (Result - 1 + 1 + 1)”, you may believe
I'm crazy ;) So here is how you should understand it : in the first
expression, Result stands for its actual value, in the line starting with
“--# check”. If you read carefully, you may notice between the line
starting with “--# assert” and the one starting with “--# check”, the is a
line “Result := Result + 1”. So, the previous value of Result, in terms of
its actual one, is “Result - 1”. In the proofs, SPARK sees Result as an
expression which is equivalent to its actual value. This expression is
relative the value of Result in the line starting with “--# assert”. So
(Result + 1 + 1) is an expression in the terms of the actual value of
Result, as the program see it would see, and (Result - 1 + 1 + 1) is the
same expression as SPARK see it. You may also, for better understanding,
read it as (previous-value-of-Result - 1 + 1 + 1).
Hope this note helped readers to understand the likely strange things they
may feel to have read here ;)
--
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
-- i.e. forget about previous premises which leads to conclusion
-- and start with new conclusion as premise.
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: SPARK : surprising failure with implication
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)
1 sibling, 0 replies; 11+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2010-06-03 11:19 UTC (permalink / raw)
Le Thu, 03 Jun 2010 10:54:51 +0200, Yannick Duchêne (Hibou57)
<yannick_duchene@yahoo.fr> a écrit:
> The original context in Ada/SPARK source is of the form (the above C1
> stands for the Check clause):
>
> --# assert ..... U'Pos (Result + 1) .....
> .....
> Result := Result + 1;
> .....
> --# check .... U'Pos (Result + 1 + 1) ....
If you meet a similar case as the above message, the only workable
workaround seems to use an intermediate variable like in:
--# assert ..... U'Pos (Result + 1) .....
.....
Previous_Result := Result;
Result := Previous_Result - 1;
.....
--# check .... U'Pos (Previous_Result + 1) ....
I suppose some of you guessed this in an extract of a loop (the Check
clause is the start of the proof of a loop invariant).
BTW, I've made a mistake in the previous transcription, this was “Result
:= Result - 1;” (sorry for that)
I will not give other examples, I will just say using intermediate
variables oftenly help with SPARK. But take care: while doing so, avoid to
introduce additional RTC VC which will turn your proof into a more
complicated story, and to avoid this misadventure, you should only use
this technique to backup previous values of a variable which is modified
since a previous Assert clause (a copy between two variables of the same
type does not introduce RTC VC, so it's OK).
Have a nice day all.
--
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
-- i.e. forget about previous premises which leads to conclusion
-- and start with new conclusion as premise.
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: SPARK : surprising failure with implication
2010-06-02 8:50 ` Yannick Duchêne (Hibou57)
2010-06-03 8:54 ` Yannick Duchêne (Hibou57)
@ 2010-06-03 16:45 ` Yannick Duchêne (Hibou57)
1 sibling, 0 replies; 11+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2010-06-03 16:45 UTC (permalink / raw)
Le Wed, 02 Jun 2010 10:50:55 +0200, Yannick Duchêne (Hibou57)
<yannick_duchene@yahoo.fr> a écrit:
I feel I have noticed a tip with substitution (people with knowledge in
SPARK implementation may confirm perhaps).
As usual, to expect to have a substitution to be applied, it is needed to
define an equality first
check A = B;
The tip takes place when the expression in which you expect the
substitution to be applied is itself an equality expression
check (... C ...) = (... A ...); -- Suppose it is proved
check (... C ...) = (... B ...); -- Seems to mostly fails
Then, it seems better to use an intermediate step and to do
check (... C ...) = (... A ...); -- Suppose it is proved
check (... A ....) = (... B ...); -- Suggest to apply the substitution
to the RHS
check (... C ...) = (... B ...); -- Use the modified RHS
--
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
-- i.e. forget about previous premises which leads to conclusion
-- and start with new conclusion as premise.
^ permalink raw reply [flat|nested] 11+ messages in thread
end of thread, other threads:[~2010-06-03 16:45 UTC | newest]
Thread overview: 11+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2010-06-01 18:51 SPARK : surprising failure with implication Yannick Duchêne (Hibou57)
2010-06-02 4:34 ` 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)
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox