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: a07f3367d7,48e1a3c594fb62e8 X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,UTF8 Path: g2news2.google.com!news4.google.com!feeder.news-service.com!news.mixmin.net!aioe.org!not-for-mail From: =?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?= =?utf-8?Q?=29?= Newsgroups: comp.lang.ada Subject: Re: SPARK Date: Tue, 18 May 2010 20:01:40 +0200 Organization: Ada At Home Message-ID: References: NNTP-Posting-Host: O/S+p4AhzNwPslgztom1bA.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: g2news2.google.com comp.lang.ada:11737 Date: 2010-05-18T20:01:40+02:00 List-Id: Le Sun, 16 May 2010 07:28:16 +0200, Yannick Duch=C3=AAne (Hibou57) = a =C3=A9crit: > Request for confirmation. > > In Praxis's documentations, there is a file named Checker_Rules.pdf, = > title is =E2=80=9CSPADE Proof Checker Rules Manual=E2=80=9D, which lis= t Checker's = > built-in rules. I do not see any reason why the Examiner/Simplifier = > would have a different rules set than the Checker, so I suppose this = > rules set is also the one used by the Examiner/Simplifier. I would jus= t = > want to be sure : someone can confirm ? > > If it is, this may explain why I meet some troubles proving one thing = = > with real arithmetic (yes, I know real arithmetic is not safe and I mu= st = > care, but this is just an exercise...) About adding rules. The Praxis document named Checker_Rules.pdf says > The tool Buildchlib is no longer shipped with the Checker > following the release of version 2.05. The use of > user-defined rule files is still permitted, through the > consult command. For further information contact > Praxis High Integrity Systems. So there is no way to add a rule system-wide as I was expecting. Attempting to change the content of an *.RUL file in the lib/checker/rul= es = directory, has no effect at all. The rules seems really compiled inside = = Simplifier and Checker. Here are the rules I was to add in NUMINEQS.RUL: 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(-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) = ]. It works only if added in an .RLU file. Note: writing something like ... inequals(124): X/Y>(-1) may_be_deduced_from [ X>=3D0, Y<0, = abs(Y)>abs(X) ]. ... although parsed correctly, will turns into a rule which may not be = applied by Simplifier. It seems rules must be given in the most = straightforward way. This may explain why ARITH.RUL contains such a thin= g: arith(1): X*1 may_be_replaced_by X. arith(2): 1*X may_be_replaced_by X. Commutativity seems not expected to be automatically applied or attempte= d. About the rules I was to add, I tried something like: inequals(122): [ X/Y>=3D0, X/Y<1 ] may_be_deduced_from [ X>=3D0,= Y>0, = Y>X ]. This is at least parsed without syntax error message, but not applied. I've noticed Simplifier seems to read an .RUL file it is belongs to a = directory where it is reading .VCG files (I don't why it do that). I've = = noticed that while I was playing a bit with it :p Will have to search for another way to add rules system-wide, if possibl= e. Have a nice day -- = There is even better than a pragma Assert: a SPARK --# check. Wanted: if you know about some though in the area of comparisons between= = SPARK and VDM, please, let me know. Will enjoy to talk with you about it= .