Prev: ANN: VC_View 2.1.1 is Linux compatible
Next: Shared library project
From: Dmitry A. Kazakov on 2 Jun 2010 04:55
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(a)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
From: Yannick Duchêne (Hibou57) on 2 Jun 2010 04:59
Le Wed, 02 Jun 2010 10:55:48 +0200, Dmitry A. Kazakov
<mailbox(a)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.
From: Yannick Duchêne (Hibou57) on 3 Jun 2010 04:54
Le Wed, 02 Jun 2010 10:50:55 +0200, Yannick Duchêne (Hibou57)
<yannick_duchene(a)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.
From: Yannick Duchêne (Hibou57) on 3 Jun 2010 05:06
Le Thu, 03 Jun 2010 10:54:51 +0200, Yannick Duchêne (Hibou57)
<yannick_duchene(a)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.
From: Yannick Duchêne (Hibou57) on 3 Jun 2010 07:19
Le Thu, 03 Jun 2010 10:54:51 +0200, Yannick Duchêne (Hibou57)
<yannick_duchene(a)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.
First  |  Prev  |  Next  |  Last
Pages: 1 2 3
Prev: ANN: VC_View 2.1.1 is Linux compatible
Next: Shared library project