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,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,463c5796782db6d8
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 2003-04-11 14:30:03 PST
Path: 
 archiver1.google.com!news1.google.com!newsfeed.stanford.edu!headwall.stanford.edu!newshub.sdsu.edu!canoe.uoregon.edu!logbridge.uoregon.edu!msunews!not-for-mail
From: "Chad R. Meiners" <crmeiners@hotmail.com>
Newsgroups: comp.lang.ada
Subject: Re: [Spark] Arrays of Strings
Date: Fri, 11 Apr 2003 17:25:09 -0400
Organization: Michigan State University
Message-ID: <b77c4b$220p$1@msunews.cl.msu.edu>
References: <slrnb95ehu.ob.lutz@taranis.iks-jena.de>
 <cf2c6063.0304110211.596b6b2b@posting.google.com>
 <1ec946d1.0304111041.7edae9a@posting.google.com>
NNTP-Posting-Host: arctic.cse.msu.edu
X-Priority: 3
X-MSMail-Priority: Normal
X-Newsreader: Microsoft Outlook Express 6.00.2800.1106
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2800.1106
Xref: archiver1.google.com comp.lang.ada:36098
Date: 2003-04-11T17:25:09-04:00
List-Id: <comp.lang.ada>


"Matthew Heaney" <mheaney@on2.com> wrote in message >
>Personally, I find Rod's solution way too heavy.
>
> Why can't Spark model an access constant to a constant object?  For
> example:

You probably could make rules to allow access constants to constant object,
but why?  Its usefulness would probably be outweighted by its added
complexity.  Furthermore, it would make the language more complicated to
learn.  If you intend on proving result about your implementation, you
should understand the implementation language so you can validate your proof
in respect to your implementations requirements.

> declare
>    X : aliased constant String := "arg1";
>    Y : aliased constant String := "arg2":
>
>    type String_Constant_Access is
>      access constant String;
>
>    type String_Constant_Access_Array is
>      (Postiive range <>) of aliased String_Constant_Access;
>
>    A : constant String_Constant_Access_Array :=
>      (X'Access, Y'Access);
> begin
>    Op (A (A'First)'Access);
> end;
>
> Everything is static.  Yes, X and Y are aliased by the components of
> array A, but neither X nor Y is variable, and the aliased view through
> A is only a constant view.  So what's the problem?

I would assume that the value added does not offset the cost to provide.

> I must say, I think the simplest solution is:
>
> exec (filename, X);  -- for argv with one arg
> exec (filename, X, Y); --for argv with two args
> etc
>

How is that so much different from Spawn(filename, X & Seperator & Y,
MySuccess); ?

> and then turn off Spark checking in the body of exec.
>
> Contrary to some of the views expressed in this thread, I find the C
> syntax perfectly natural and perfectly elegant.  Rod's solution is
> neither.

Rod's solution is correct though; furthermore, it isn't too heavy since all
the work in deciding what needs to be proved and what will be left unproved
needs to be done explicitly one way or the other.