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 05:19:05 PST
Path: 
 archiver1.google.com!news1.google.com!sn-xit-02!sn-xit-06!sn-xit-08!supernews.com!news-out.visi.com!petbe.visi.com!uunet!ash.uu.net!spool0900.news.uu.net!reader0900.news.uu.net!not-for-mail
Date: Fri, 11 Apr 2003 08:19:00 -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>
 <1049908902.143649@master.nyc.kbcfp.com>
 <0AF16DC5CF0F5631.90C7740553757FCD.D1A6F4ACFB3596A1@lp.airnews.net>
In-Reply-To: 
 <0AF16DC5CF0F5631.90C7740553757FCD.D1A6F4ACFB3596A1@lp.airnews.net>
Content-Type: text/plain; charset=us-ascii; format=flowed
Content-Transfer-Encoding: 7bit
Organization: KBC Financial Products
Message-ID: <1050063540.619475@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: 1050063541 reader0.ash.ops.us.uu.net 12010 204.253.250.10
Xref: archiver1.google.com comp.lang.ada:36085
Date: 2003-04-11T08:19:00-04:00
List-Id: <comp.lang.ada>

John R. Strohm wrote:
> When you declare an array to be of a given size, you create a proof
> obligation that the subscript expression will always be in bounds.
> Satisfying this proof obligation is what you do during verification.


Sure, I understand what program proof and verification are about.

What I'm suggesting is that there is a tension between normal Ada
usage, which is to declare your types "snugly" so that they hold
only the ranges you expect them to have, and programs which will
always be verified before they are permitted to run.