Re: SPARK : surprising failure with implication

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

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.