Re: [Spark] Converting Arrays

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

* JP Thornley wrote:
>* Lutz Donnerhacke <lutz@iks-jena.de> writes
>>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.
>
> Note that here you have given two different replacements for the same 
> item. It is not obvious what the Simplifier will do with these.

I did this after some testing.

> The restriction that an out mode parameter can't be referenced in a
> precondition seems to be the major cause of the difficulty,

The constraints of an unconstraint OUT type are IN parameters. Spark does
not reflect this. => Problem.

> and I have (reluctantly) come to the conclusion that the way to avoid
> explicit rules for each instance of the output parameter is to pass the
> length as an additional parameter, as Rod suggests.

This is not really acceptable, because it seperates information crutial for
proofing exeption freedom from the objects. This renders the whole proof
useless.

But even the much more simple example does not work:
with Spark_IO;
--# inherit Spark_IO;

--# main_program;
procedure main
  --# global in out Spark_IO.Outputs;
  --# derives Spark_IO.Outputs from Spark_IO.Outputs;
  is
   subtype My_Index is Positive range 1 .. 5;
   subtype My_String is String(My_Index);
   my : My_String;
   world : constant My_String := "Hello";
   
   procedure Copy(s : String; d : out String)
     --# derives d from s;
     --# pre s'Length = My_String'Length;
     is
      --# hide Copy;
   begin
      d := s;
   end Copy;
begin
   Copy(world, my);
   Spark_IO.Put_Line(Spark_IO.Standard_Output, my, 0);
end main;

It does not matter, how the parameters of Copy are given in the main program.
The examiner does not generate the correct rules in the calling enviroment.
It fails to transform the called parameters by the calling ones. :-(

Of course the simple change to constraint arrays works like a charm:
with Spark_IO;
--# inherit Spark_IO;

--# main_program;
procedure main
  --# global in out Spark_IO.Outputs;
  --# derives Spark_IO.Outputs from Spark_IO.Outputs;
  is
   subtype My_Index is Positive range 1 .. 5;
   subtype My_String is String(My_Index);
   my : My_String;
   world : constant My_String := "Hello";
   
   procedure Copy(s : My_String; d : out My_String)
     --# derives d from s;
     --# pre s'Length = My_String'Length;
     is
   begin
      d := s;
   end Copy;
begin
   Copy(world, my);
   Spark_IO.Put_Line(Spark_IO.Standard_Output, my, 0);
end main;