Re: Lost in translation (with SPARK user rules)

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

Le Sun, 30 May 2010 01:03:31 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:
> 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 didn't wanted to add rules for all constants, like 256, and etc.  
Fortunately, there is a somewhat cleaner way to work around, which still  
involves a constant, but a nice one : 2.

If “my_rule(1): ((X ** Y) < (X ** Z)) -> (Y < Z) may_be_deduced_from  
[...].” is completed with another rule like, “my_rule(2): ((2 ** Y) < (2  
** Z)) -> (Y < Z) may_be_deduced_from [...].”, then it did not change  
anymore 2 ** 8 into 256 and see a match.

I don't know what it do in the background, nor why it preserve the  
expression when the rule to match contains at least a constant, however,  
what is nice with this work around, it that it will work with all powers  
of two.

I still would like to know about the details : why when X is replaced by  
the literal 2, it does not match the same way ?

Important to notice anyway.

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