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-09 10:21:44 PST
Path: 
 archiver1.google.com!news1.google.com!newsfeed.stanford.edu!headwall.stanford.edu!newshub.sdsu.edu!canoe.uoregon.edu!arclight.uoregon.edu!news.tufts.edu!uunet!dca.uu.net!ash.uu.net!spool0901.news.uu.net!spool0900.news.uu.net!reader0902.news.uu.net!not-for-mail
Date: Wed, 09 Apr 2003 13:21:41 -0400
From: Hyman Rosen <hyrosen@mail.com>
User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.0; en-US;
 rv:1.4a) Gecko/20030302
X-Accept-Language: en-us, en
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: [Spark] Arrays of Strings
References: <slrnb95ehu.ob.lutz@taranis.iks-jena.de>
 <pan.2003.04.08.18.08.55.205947@T-Online.de>
 <slrnb97pl4.or.lutz@taranis.iks-jena.de>
 <1049891888.75004@master.nyc.kbcfp.com>
 <b714ol$9v3of$1@ID-175126.news.dfncis.de>
In-Reply-To: <b714ol$9v3of$1@ID-175126.news.dfncis.de>
Content-Type: text/plain; charset=us-ascii; format=flowed
Content-Transfer-Encoding: 7bit
Organization: KBC Financial Products
Message-ID: <1049908902.143649@master.nyc.kbcfp.com>
Cache-Post-Path: master.nyc.kbcfp.com!unknown@fixedcost.nyc.kbcfp.com
X-Cache: nntpcache 3.0.1 (see http://www.nntpcache.org/)
NNTP-Posting-Host: 204.253.250.10
X-Trace: 1049908903 reader2.ash.ops.us.uu.net 17071 204.253.250.10
Xref: archiver1.google.com comp.lang.ada:36025
Date: 2003-04-09T13:21:41-04:00
List-Id: <comp.lang.ada>

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