From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.4
X-Google-Thread: 103376,ec6f74e58e86b38b,start
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,UTF8
Path: 
 g2news1.google.com!news4.google.com!proxad.net!feeder1-2.proxad.net!usenet-fr.net!gegeweb.org!aioe.org!not-for-mail
From: =?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?=
 =?utf-8?Q?=29?=
 <yannick_duchene@yahoo.fr>
Newsgroups: comp.lang.ada
Subject: Lost in translation (with SPARK user rules)
Date: Wed, 26 May 2010 12:09:17 +0200
Organization: Ada At Home
Message-ID: <op.vda45rsfule2fv@garhos>
NNTP-Posting-Host: 2gba2B6ZhmveiNSbnmeIoQ.user.speranza.aioe.org
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed; delsp=yes
Content-Transfer-Encoding: Quoted-Printable
X-Complaints-To: abuse@aioe.org
X-Notice: Filtered by postfilter v. 0.8.2
User-Agent: Opera Mail/10.53 (Win32)
Xref: g2news1.google.com comp.lang.ada:11049
Date: 2010-05-26T12:09:17+02:00
List-Id: <comp.lang.ada>

Lost in translation... do you know the movie ?

No, I'm joking, this is not about this 2002 movie, that's about SPARK, a=
nd  =

exactly, about translating some expressions in the rules language.

Previously, I have successfully added these rules, in an *.RLU file:

    inequals(122):  X/Y<1     may_be_deduced_from [ X>=3D0, Y>0, Y>X ].
    inequals(123):  X/Y<1     may_be_deduced_from [ X<=3D0, Y<0, Y<X ].
    inequals(124):  X/Y>(-1)  may_be_deduced_from [ X>=3D0, Y<0, (-Y)>X =
].
    inequals(125):  X/Y>(-1)  may_be_deduced_from [ X<=3D0, Y>0, Y>(-X) =
].


I wanted to do the same, for another kind of rule, about bitwise. The ru=
le  =

I wanted to add is something like:
(X and 2 ** N) =3D 0 may be deduced from ((X / (2 ** N)) and 1) =3D 0
and the opposite

I tried with this:

    bitwise(112): bit__and(X div (2**N), 1)=3D0 may_be_deduced_from [  =

(bit__and(X, 2**N)=3D0), X>=3D0, N>=3D0 ].
    bitwise(113): bit__and(X, 2**N)=3D0 may_be_deduced_from [ (bit__and(=
X div  =

(2**N), 1)=3D0), X>=3D0, N>=3D0 ].

But this fails, although the simplifier does not returns me any syntax  =

error messages about this *.RLU file. This fails, because it cannot prov=
e  =

something like this:

    --# check ((Instance and 2) =3D 0) -> (((Instance / 2) and 1) =3D 0)=
;

The latter should be directly deduced from the two previous rules if the=
se  =

were OK. So I suppose something is wrong with these rules, and the  =

expression in =E2=80=9C[...]=E2=80=9D is not interpreted the way it seem=
s to be to me.

One entertaining thing: I've noticed =E2=80=9Cand 1=E2=80=9D is always r=
eplaced by =E2=80=9Cmod 2=E2=80=9D  =

in the simplifier's *.SIV output files. As an example, the latter Check =
 =

clause is replaced by:

    C1:    bit__and(instance, 2) =3D 0 -> instance div 2 mod 2 =3D 0 .