Re: [Spark] Arrays of Strings

[Hyman Rosen <hyrosen@mail.com>]

Vinzent Hoefler wrote:
> The reliability is not in the subset like in MISRA-C, it is in the
> static analysis. I think, it is called *proof*.

I am starting to be a little disturbed now that I've thought about
this a little more. You seem to be telling me that it's OK to have
variables declared loosely (Natural instead of the array range type)
becuase a program verifier will notice problems regardless. To me,
this seems contrary to to the design of Ada, which emphasizes saying
what you mean using the type system. I've been told here frequently
that Ada's style lends itself to avoiding buffer overflows because
you declare variables that loop over array ranges, and so there is
never an opportunity to go off the end.

I find that the posted code looks very much like something you would
see in C (except for that awful buffer setting stuff).