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 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,UTF8 Path: g2news1.google.com!news1.google.com!news3.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?= Newsgroups: comp.lang.ada Subject: Re: Lost in translation (with SPARK user rules) Date: Wed, 26 May 2010 12:57:11 +0200 Organization: Ada At Home Message-ID: References: <0466e131-cc80-4db4-b080-eec9aefcb1c7@z17g2000vbd.googlegroups.com> 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:11054 Date: 2010-05-26T12:57:11+02:00 List-Id: Le Wed, 26 May 2010 12:38:52 +0200, Phil Thornley = a =C3=A9crit: > I don't think there us anything wrong with these rules, but the > Simplifier will not use a *combination* of user rules to discharge a > proof. (They are not as 'powerful' as the built-in rules as they are > not consulted until the Simplifier has tried all its other > strategies). > > For example, section 7.3.1 of the Simplifier User Manual says: > "For an inference rule of the form > rulename(1): Goal may_be_deduced_from Conditions. > the Simplifier will attempt to find a means of instantiating > all of the wildcards in Goal such that it becomes an exact > match for an existing undischarged conclusion." > > This means that a single inference rule is applied only if it > *directly* matches a conclusion. > > Also, since user rules are applied right at the end, you have to use > the form of the conclusion as it appears in the SIV file, so: >> One entertaining thing: I've noticed =E2=80=9Cand 1=E2=80=9D is alway= s replaced 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 = . > > If that is the conclusion left in the SIV file then the user rule to > prove it is: > user_bitwise(1): bit__and(X, 2) =3D 0 -> X div 2 mod 2 =3D 0 > may_be_deduced . I remember about this, this was just that I did not suspected this had t= o = be a so exact match. > (and a minor comment is that it is probably not a good idea to use the= > Proof Checker rule family names for Simplifier user rules - it just > adds to the confusion about how the rules are used.) Oops, sorry, I though this was better to go on with an existing naming = convention already established. Overall so far to me. I don't know what to think about one feeling, may be I'm wrong: I feel a= = bit discouraged with SPARK now. I wonder if this is really this thing I = = was waiting for so long (I am referring to some of my previous words abo= ut = it in another thread). May be I should give up with it. If I could believe they could be some funding or a market for that, I = would like to work on another system in this area... but I don't think s= o = (I don't think there are many people expecting this kind of things). Well, for the time being, I feel I gonna forget about it at least for so= me = time and go on without it. -- = There is even better than a pragma Assert: a SPARK --# check.