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 03:57:04 PST Path: archiver1.google.com!news1.google.com!newsfeed.stanford.edu!news-spur1.maxwell.syr.edu!news.maxwell.syr.edu!newsfeed.icl.net!newsfeed.fjserv.net!news-FFM2.ecrc.net!news.iks-jena.de!not-for-mail From: Lutz Donnerhacke Newsgroups: comp.lang.ada Subject: Re: [Spark] Converting Arrays Date: Wed, 12 Mar 2003 11:57:04 +0000 (UTC) Organization: IKS GmbH Jena Message-ID: References: <3e6ef2ad$1@baen1673807.greenlnk.net> NNTP-Posting-Host: taranis.iks-jena.de X-Trace: branwen.iks-jena.de 1047470224 25841 217.17.192.37 (12 Mar 2003 11:57:04 GMT) X-Complaints-To: usenet@iks-jena.de NNTP-Posting-Date: Wed, 12 Mar 2003 11:57:04 +0000 (UTC) User-Agent: slrn/0.9.7.4 (Linux) Xref: archiver1.google.com comp.lang.ada:35250 Date: 2003-03-12T11:57:04+00:00 List-Id: * Phil Thornley wrote: > "JP Thornley" wrote in message >> 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). Good idea. In order to make it handy rule files must be regenerated by a perl script. > 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, There are quite a lot of other problems which can be solved in this way. I.e. transfering user defined ranges from one file to an other in order to be checked there. > 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 :-). Of course. And you have to be very familar with the verification language. > 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.) I'd like to see it working an any way, currently it's boring. > Then 'consult' this file in the Checker and use the rule in a 'replace' > command. I do not have the Checker yet. > 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. length_of_xxx is a bad concept anyway, because it has to be generated for every unconstraint out parameter seperately. (Unless you name them uniquely.) My tests result in the following program: cat > test.ads < test.adb < main.adb < main.idx < C1: test_it__src__last - test_it__src__first + 1 = test_it__dest__last - test_it__dest__first + 1 . For path(s) from start to run-time check associated with statement of line 15: procedure_main_2. H1: true . H2: test_it__src__last - test_it__src__first + 1 = test_it__dest__last - test_it__dest__first + 1 . H3: for_all (i___1: integer, ((i___1 >= positive__first) and ( i___1 <= positive__last)) -> ((element(my__1, [ i___1]) >= character__first) and (element(my__1, [ i___1]) <= character__last))) . -> C1: 0 >= natural__first . C2: 0 <= natural__last . For path(s) from start to finish: procedure_main_3. *** true . /* trivially true VC removed by Examiner */ Trying the other variant cat > test.ads < C1: test_it__src__last - test_it__src__first + 1 = test__length_of_dest . For path(s) from start to run-time check associated with statement of line 15: procedure_main_2. H1: true . H2: test_it__src__last - test_it__src__first + 1 = test__length_of_dest . H3: for_all (i___1: integer, ((i___1 >= positive__first) and ( i___1 <= positive__last)) -> ((element(my__1, [ i___1]) >= character__first) and (element(my__1, [ i___1]) <= character__last))) . -> C1: 0 >= natural__first . C2: 0 <= natural__last . For path(s) from start to finish: procedure_main_3. *** true . /* trivially true VC removed by Examiner */ Adding a rule to main.rls: $ echo >> main.rls " main_rules(100): test__length_of_dest may_be_replaced_by test_it__dest__last - test_it__dest__first + 1. main_rules(101): test__length_of_dest may_be_replaced_by my__last - my__first + 1. " $ sparksimp $ diff -u main.siv* --- main.siv 2003-03-12 12:47:03.000000000 +0100 +++ main.siv- 2003-03-12 12:43:44.000000000 +0100 @@ -5,7 +5,7 @@ ******************************************************* - CREATED 12-MAR-2003, 12:43:31 SIMPLIFIED 12-MAR-2003, 12:47:00 + CREATED 12-MAR-2003, 12:43:31 SIMPLIFIED 12-MAR-2003, 12:43:41 (Simplified by SPADE Simplifier, Demo Version) procedure main @@ -19,15 +19,13 @@ procedure_main_1. H1: true . -> -C1: test_it__src__last - test_it__src__first + 1 = test_it__dest__last - - test_it__dest__first + 1 . +C1: test_it__src__last - test_it__src__first + 1 = test__length_of_dest . [...] Which is correct, but does not solve the problem. How do I this correctly? I believe there is a much more difficult problem in this area, because the more simple assertion: --# pre src'Length = 5; results in C1: test_it__src__last - test_it__src__first + 1 = 5 . (vcg) and C1: test_it__src__last - test_it__src__first = 4 . (siv) IMHO the substitution of the formal parameter by the calling enviroment is missing.