Prev: ANN: VC_View 2.1.1 is Linux compatible
Next: Shared library project
From: Yannick Duchêne (Hibou57) on 3 Jun 2010 12:45
Le Wed, 02 Jun 2010 10:50:55 +0200, Yannick Duchêne (Hibou57)
<yannick_duchene(a)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.
First  |  Prev  | 
Pages: 1 2 3
Prev: ANN: VC_View 2.1.1 is Linux compatible
Next: Shared library project