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 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,744136b4fae1ff3e X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2003-03-12 00:42:53 PST Path: archiver1.google.com!news1.google.com!newsfeed.stanford.edu!news-spur1.maxwell.syr.edu!news.maxwell.syr.edu!news-out.visi.com!petbe.visi.com!uunet!ash.uu.net!lore.csc.com!baen1673807.greenlnk.net!baen1673807!not-for-mail From: "Phil Thornley" Newsgroups: comp.lang.ada Subject: Re: [Spark] Converting Arrays Date: Wed, 12 Mar 2003 08:43:17 -0000 Organization: Computer Sciences Corporation Message-ID: <3e6ef2ad$1@baen1673807.greenlnk.net> References: NNTP-Posting-Host: 20.44.241.70 X-Trace: lore.csc.com 1047458571 169 20.44.241.70 (12 Mar 2003 08:42:51 GMT) X-Complaints-To: abuse@news.csc.com NNTP-Posting-Date: Wed, 12 Mar 2003 08:42:51 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 5.00.2919.6600 X-MimeOLE: Produced By Microsoft MimeOLE V5.00.2919.6600 X-Original-NNTP-Posting-Host: waec857.wa.bae.co.uk X-Original-Trace: 12 Mar 2003 08:41:17 GMT, waec857.wa.bae.co.uk Xref: archiver1.google.com comp.lang.ada:35243 Date: 2003-03-12T08:43:17+00:00 List-Id: "JP Thornley" wrote in message news:ON9GtiBcskb+IwAh@diphi.demon.co.uk... > You can then write the proof rule for Length_Of_Path: > to_fullpath_rules(100): length_of_path may_be_replaced_by > path__last - path__first + 1 . > > Append this to the generated rule file before running the Simplifier. > (The rule number needs to be larger than the highest rule number > generated by the Examiner). Perhaps I should add that this is a slightly quick and dirty way of getting the proof rule in. It has the advantage that the Simplifier will be able to use it, but the disadvantage that the rule has to be created for every subprogram that calls To_Fullpath as well as for To_Fullpath itself (and I'm sure that no-one would ever contemplate creating a different rule for different situations :-). The more 'correct' way is to write a new rule family. Create a file called (say) test.rls with contents: rule_family test: X requires [X:any]. test_rule(1): length_of_path may_be_replaced_by path__last - path__first + 1 . (Warning - the above is as written, and unchecked.) Then 'consult' this file in the Checker and use the rule in a 'replace' command. The advantage of this is that the rule is only written once, so there can't be any mistakes made in duplicating it, but has the disadvantage that the Simplifier won't be able to do anything with 'length_of_path' and you end up with more VCs to prove in the Checker. Cheers, Phil -- Phil Thornley BAE SYSTEMS