Re: [Spark] Arrays of Strings

["Chad R. Meiners" <crmeiners@hotmail.com>]

"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.