Re: [Spark] Converting Arrays

[Lutz Donnerhacke <lutz@iks-jena.de>]

* Phil Thornley wrote:
> "JP Thornley" <jpt@diphi.demon.co.uk> 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 <<END
package test is
   --# function Length_Of_Dest return Integer;
   procedure Test_It (src : String; dest : out String);
   --# derives dest from src;
   --# pre src'Length = dest'Length;
end test;
END
cat > test.adb <<END
package body test is
   procedure Test_It (src : String; dest : out String) is
      --# hide Test_It;
   begin
      dest := src;
   end Test_It;
end test;
END
cat > main.adb <<END
with test, Spark_IO;
--# inherit test, Spark_IO;
--# main_program;
procedure main
  --# global in out Spark_IO.Outputs;
  --# derives Spark_IO.Outputs from Spark_IO.Outputs;
  is
   subtype Test_Len is Positive range 1 .. 5;
   subtype Test_String is String(Test_Len);

   my : Test_String;
begin
   test.Test_It("Hallo", my);
   Spark_IO.Put_Line(Spark_IO.Standard_Output, my, 0);
end main;
cat > main.idx <<END
Spark_IO specification is in .../spark_io.ads
Spark_IO body          is in .../spark_io.adb
test     specification is in test.ads
test     body          is in test.adb
END


Running "spark -i=main.idx -e main.adb" results in the expected error
message, but generates the right VC!
$ cat main.vcg
          *******************************************************
                      Semantic Analysis of SPARK Text
       SPARK95 Examiner with VC and RTC Generator Release 6.3 / 11.02
                           Demonstration Version
          *******************************************************


                       DATE : 12-MAR-2003 12:32:31.79

                               procedure main




For path(s) from start to precondition check associated with statement of line 14:

procedure_main_1.
H1:    true .
        ->
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 <<END
package test is
   --# function Length_Of_Dest return Integer;
   procedure Test_It (src : String; dest : out String);
   --# derives dest from src;
   --# pre src'Length = Length_Of_Dest;
end test;
END

results in
$ cat main.vcg
          *******************************************************
                      Semantic Analysis of SPARK Text
       SPARK95 Examiner with VC and RTC Generator Release 6.3 / 11.02
                           Demonstration Version
          *******************************************************


                       DATE : 12-MAR-2003 12:43:31.25

                               procedure main




For path(s) from start to precondition check associated with statement of line 14:

procedure_main_1.
H1:    true .
        ->
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.