Re: Lost in translation (with SPARK user rules)

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

Le Thu, 27 May 2010 12:55:04 +0200, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:
> And Simplifier fails to prove Check #3 ; an excerpt of the *.SIV file  
> shows why (conclusion associated to Check #3):
>
>     C1:    bit__and(v, 1) = 0 or bit__and(v, 1) = 1 .

Ok, found. I was not correct with the way to require the type to be  
integer as done in

    my_set(1): (X=0) or (X=1) may_be_deduced_from [ integer(X), X>=0, X<=1  
].

It has to be

    my_set(1): (X=0) or (X=1) may_be_deduced_from [  
goal(checktype(X,integer)), X>=0, X<=1 ].

I've check that

    my_set(1): (X=0) or (X=1) may_be_deduced_from [ goal(integer(X)), X>=0,  
X<=1 ].

does not work, which lead to another question : what is the difference  
between the two predicates “integer(X)” and “checktype(X,integer)” ? The  
documentation is not clear to me about it. About “checktype(EXPRESSION,  
TYPE_IDENTIFIER)”, it says “This predicate may be used to check that an  
expression is of an appropriate type” and about “integer(EXPRESSION)” is  
says This built-in Prolog predicate succeeds if and only if its argument  
is instantiated to an integer. So what's the difference between  
“goal(integer(X))” and “goal(checktype(X,integer))”. Does the latter  
refers to root type as defined in source and the other to something else ?  
(so what?)

Another strange thing is that the file NUMINEQS.RUL does not contains any  
predicate stating arguments have to be integers and there is just a  
comment in heading, nothing in rules about it.

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