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-13 02:14:38 PST
Path: 
 archiver1.google.com!news1.google.com!newsfeed.stanford.edu!logbridge.uoregon.edu!news-FFM2.ecrc.net!news.iks-jena.de!not-for-mail
From: Lutz Donnerhacke <lutz@iks-jena.de>
Newsgroups: comp.lang.ada
Subject: Re: [Spark] Converting Arrays
Date: Thu, 13 Mar 2003 10:14:37 +0000 (UTC)
Organization: IKS GmbH Jena
Message-ID: <slrnb70mgb.nv.lutz@taranis.iks-jena.de>
References: <slrnb6phge.1gd.lutz@taranis.iks-jena.de>
 <cf2c6063.0303110214.5c978575@posting.google.com>
 <slrnb6rfur.nq.lutz@taranis.iks-jena.de> <ON9GtiBcskb+IwAh@diphi.demon.co.uk>
 <3e6ef2ad$1@baen1673807.greenlnk.net>
 <slrnb6u84d.nt.lutz@taranis.iks-jena.de> <qT5vqLJMC4b+IwF9@diphi.demon.co.uk>
NNTP-Posting-Host: taranis.iks-jena.de
X-Trace: branwen.iks-jena.de 1047550477 1528 217.17.192.37 (13 Mar 2003
 10:14:37 GMT)
X-Complaints-To: usenet@iks-jena.de
NNTP-Posting-Date: Thu, 13 Mar 2003 10:14:37 +0000 (UTC)
User-Agent: slrn/0.9.7.4 (Linux)
Xref: archiver1.google.com comp.lang.ada:35283
Date: 2003-03-13T10:14:37+00:00
List-Id: <comp.lang.ada>

* 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;