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=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,da7583a21995901b X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.66.90.102 with SMTP id bv6mr2637739pab.34.1345031535212; Wed, 15 Aug 2012 04:52:15 -0700 (PDT) Path: c10ni116599pbw.0!nntp.google.com!news1.google.com!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail From: Ben Hocking Newsgroups: comp.lang.ada Subject: Re: Using .rlu files in SPARK Ada Date: Wed, 15 Aug 2012 04:50:34 -0700 (PDT) Organization: http://groups.google.com Message-ID: <75429d4f-fe7c-4546-baca-f424679f3452@googlegroups.com> References: NNTP-Posting-Host: 8.25.3.17 Mime-Version: 1.0 X-Trace: posting.google.com 1345031535 24237 127.0.0.1 (15 Aug 2012 11:52:15 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Wed, 15 Aug 2012 11:52:15 +0000 (UTC) Cc: phil.jpthornley@gmail.com In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=8.25.3.17; posting-account=hKGsDAoAAAC9HB_9misjykjawYQeT_yf User-Agent: G2/1.0 Content-Type: text/plain; charset=ISO-8859-1 Date: 2012-08-15T04:50:34-07:00 List-Id: On Monday, August 13, 2012 11:46:04 AM UTC-4, Phil Thornley wrote: > In article , > > Ben says... > > > > > > I'm trying to satisfy all of the Verification Conditions that SPARK Ada generates in some code of mine. > > > > > > I've been unable to satisfy the following check statement: > > > a2 := x3 - x1; > > > b := y3 - y1; > > > --# check b < a2 -> (b rem a2 = b); > > > > > > It generates the following VC: > > > y3 - y1 < x3 - x1 -> y3 - y1 - (y3 - y1) div (x3 - x1) * (x3 - x1) = y3 - y1 > > > > > > In my .rlu file (which I know is being read because other rules are being applied, and I see it mentioned in my .slg file), I have: > > > small_rem: y3 - y1 - (y3 - y1) div (x3 - x1) * (x3 - x1) = (y3 - y1) may_be_deduced_from [y3 - y1 < x3 - x1]. > > > > To avoid any additional complications, I'll start by assuming that a2 > > and b are guaranteed to be Positive (and there should really be > > something in the rule for that). > > > > For a deduction rule to work, the formula that is deduced has to match > > the conclusion and the sideconditions have to match hypotheses (or be > > provable from the hypotheses). > > > > This rule would work if the equality was the conclusion and > > y3 - y1 < x3 - x1 were a hypothesis. > > > > Since the conclusion is an implication, that is what the rule must be. > > > > So you can either use: > > small_rem: y3 - y1 < x3 - x1 -> y3 - y1 - (y3 - y1) div (x3 - x1) * (x3 > > - x1) = (y3 - y1) may_be_deduced . > > > > or change the code to: > > a2 := x3 - x1; > > b := y3 - y1; > > if b < a2 then > > --# check b rem a2 = b; > > null; > > end if; > > > > (I have occasionally used null conditional statements to avoid complex > > implications.) > > > > > > > > (Note that I originally had: > > > small_rem: x rem y = x may_be_deduced_from [x < y]. > > > > > > However, in an effort to rule out any possible source of confusion, I expanded it to exactly what I was seeing in the .siv file.) > > > > > > Am I doing something incorrectly, or is there some limitation of SPARK here? > > > > This never had a chance of working because rem is not an FDL operator > > (which is why the Examiner expands it out.) > > > > However you also need to understand the use of wildcards in rules. This > > is covered in Section 7 of the Simplifier User Manual, but, briefly, > > anything in lower case in a rule formula has to match the text of the VC > > precisely (so the above rule would not work if you changed any of x1, > > x3, y1, y3 to something else). > > > > Any name in a rule that starts with an upper-case character is a wild- > > card (aka 'Prolog variable') that can be matched to any expression > > within a VC, so the ideal rule for your present code is probably: > > small_rem: A < B -> A - A div B * B = A may_be_deduced . > > > > or, to make sure it doesn't get used incorrectly anywhere else: > > small_rem: A < B -> A - A div B * B = A may_be_deduced_from > > [A >= 0, B > 0, > > goal(checktype(A, integer)), > > goal(checktype(B, integer)) ] . > > > > (and there's probably another for negative A and B as well). > > > > Warning: all above expressions typed without any checking with SPARK > > tools. > > > > Cheers, > > > > Phil Thanks, Phil. That solved my problem. Best regards, -Ben