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=3.0 required=5.0 tests=BAYES_00,DATE_IN_PAST_24_48, FORGED_GMAIL_RCVD,FREEMAIL_FROM,FREEMAIL_REPLYTO,REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,da7583a21995901b X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.101.152.24 with SMTP id e24mr2718773ano.0.1344998913205; Tue, 14 Aug 2012 19:48:33 -0700 (PDT) Path: c6ni115604019qas.0!nntp.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!nrc-news.nrc.ca!goblin1!goblin2!goblin.stu.neva.ru!news.stack.nl!dedekind.zen.co.uk!zen.net.uk!hamilton.zen.co.uk!reader01.nrc01.news.zen.net.uk.POSTED!not-for-mail From: Phil Thornley Newsgroups: comp.lang.ada Subject: Re: Using .rlu files in SPARK Ada Date: Mon, 13 Aug 2012 16:46:04 +0100 Message-ID: References: Reply-To: phil.jpthornley@gmail.com MIME-Version: 1.0 User-Agent: MicroPlanet-Gravity/3.0.4 Organization: Zen Internet NNTP-Posting-Host: 05fc4882.news.zen.co.uk X-Trace: DXC=fC4hEEQ?9Z5FiQn`d_;:_;a0UP_O8AJo<=dR0\ckLKG0WeZ<[7LZNR6;^>bE\k^nk8UhLi?]0KG=;44PD4LLEW`4O^>2jRX?:U9 X-Complaints-To: abuse@zen.co.uk Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Date: 2012-08-13T16:46:04+01:00 List-Id: In article , benjaminhocking@gmail.com 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