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:

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.