Re: Lost in translation (with SPARK user rules)

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

Le Wed, 26 May 2010 12:09:17 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:
> Lost in translation... do you know the movie ?

> No, I'm joking, this is not about this 2002 movie, that's about SPARK,  
> and exactly,
> about translating some expressions in the rules language.
> [...]

In this area, the Simplifier sometimes shows slight capacities to be  
boring.

Let a Check clause be “--# check ((2 ** Count) < (2 ** 8)) -> (Count < 8);”
Let a user rule be “my_rule: ((X ** Y) < (X ** Z)) -> (Y < Z)  
may_be_deduced_from [some-obvious-conditions].”

There should be an exact match, isn't it ?

Well, I guess you guess: it fails to prove the Check clause. Now, if you  
would like to know why, here is: it replaces this by “2 ** count < 256 ->  
count < 8”, ... it turns “(2 ** 8)” into “256”, so that it can't see any  
more an exact match with the user rule

I've check in the *.SLG file, this is indeed due to simplification, this  
is not due to an hypothetical related error.


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