Re: Lost in translation (with SPARK user rules)

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

Le Wed, 26 May 2010 12:57:11 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:
>> If that is the conclusion left in the SIV file then the user rule to
>> prove it is:
>>    user_bitwise(1): bit__and(X, 2) = 0 -> X div 2 mod 2 = 0
>> may_be_deduced .
> I remember about this, this was just that I did not suspected this had  
> to be a so exact match.
Finally, there is a work-around: if the Simplifier expect an expression  
which exactly match the one provided as a user rule, and there is not a  
direct matching expression in the source, then just use Simplifier's  
embedded rules to prove an expression is equivalent to the one the  
Simplifier expect an exact match.

That is, if there a user rule of the form

    my_rule(1) Conclusion_1 may_be_deduced_from [Expression_1].

and the source unfortunately contains only

    Expression_2

then try something like

    --# check Expression_2 -> Intermediate_Expression(1);
    --# check ...;
    --# check ...;
    --# check Intermediate_Expression(N) -> Expression_1;

and here it is.

-- 
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.