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,ec6f74e58e86b38b X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,CP1252 Path: g2news2.google.com!postnews.google.com!j12g2000pri.googlegroups.com!not-for-mail From: Phil Thornley Newsgroups: comp.lang.ada Subject: Re: Lost in translation (with SPARK user rules) Date: Sun, 30 May 2010 02:26:12 -0700 (PDT) Organization: http://groups.google.com Message-ID: <927d98bd-9219-426d-815a-392c28211908@j12g2000pri.googlegroups.com> References: NNTP-Posting-Host: 80.177.171.182 Mime-Version: 1.0 Content-Type: text/plain; charset=windows-1252 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1275211572 2432 127.0.0.1 (30 May 2010 09:26:12 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Sun, 30 May 2010 09:26:12 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: j12g2000pri.googlegroups.com; posting-host=80.177.171.182; posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.1; WOW64; Trident/4.0; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR 3.0.30729; Media Center PC 6.0),gzip(gfe) Xref: g2news2.google.com comp.lang.ada:12158 Date: 2010-05-30T02:26:12-07:00 List-Id: On 30 May, 00:03, Yannick Duch=EAne (Hibou57) wrote: > In this area, the Simplifier sometimes shows slight capacities to be =A0 > boring. > > Let a Check clause be =93--# check ((2 ** Count) < (2 ** 8)) -> (Count < = 8);=94 > Let a user rule be =93my_rule: ((X ** Y) < (X ** Z)) -> (Y < Z) =A0 > may_be_deduced_from [some-obvious-conditions].=94 > > There should be an exact match, isn't it ? > > Well, I guess you guess: it fails to prove the Check clause. Now, if you = =A0 > would like to know why, here is: it replaces this by =932 ** count < 256 = -> =A0 > count < 8=94, ... it turns =93(2 ** 8)=94 into =93256=94, so that it can'= t see any =A0 > more an exact match with the user rule > > I've check in the *.SLG file, this is indeed due to simplification, this = =A0 > is not due to an hypothetical related error. The full description of all the simplification steps is in section 3 of the Simplifier User Manual, so if you read this and follow through the steps in a simplification log file then you should get a better understanding of how the tool works - and so how to write user rules that are effective. Application of user rules is the final step (out of about a dozen) that the Simplifier uses, so at that point a conclusion is likely to have been changed from the form of the annotation that generated it. In the case you describe here Count must be defined as a constant with value 8, and that replacement is the first step that the Simplifier takes. Then it will convert 2**8 to 256 in a subsequent step. (A basic strategy of the Simplifier is to replace any expressions with a simpler version wherever possible - perhaps that's why it called the Simplifier rather than the 'Prover' :-). Section 3.12 describes how the Simplifier uses user rules - and it is clear from this description that the rule needs to match expressions in the VC as they are at the end of the process, not as in the original VC. You can see why this is sensible (even if it has some drawbacks*). Generally the way that a user rule is written is in response to an unproven conclusion in a simplified VC, so the author of the rule uses the final form of the unproven VC to write the rule. Therefore the rule can only be reliably applied at the point where the VC has reached its final form. I guess it might be possible for the Simplifier to try all the user rules at each stage of the process - but the developers of the tool have been concentrating heavily on making simplification as quick as possible (quite rightly in my view) and would not want to do anything that might slow it down without a very strong argument for the advantages of doing that. * The main drawback that I see is that some user rules define replacements that must be made for the VC to be provable, but at present these are made too late for them to be effective, since the Simplifier has already exhausted all its other strategies. It would be nice to have replacements defined in user rules applied in the first simplification stage, how about: my_rewrite(1): A must_be_replaced_by B if [...] . (Of course nothing is ever simple, for example what happens if one rewrite rule requires another to be applied before its sideconditions are satisfied - are all such rules tried repeatedly until none are used, or is it a once-only pass? etc...) Cheers, Phil