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 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 06:31:05 PST
Path: 
 archiver1.google.com!news1.google.com!sn-xit-02!sn-xit-03!sn-xit-01!sn-xit-08!supernews.com!news.airnews.net!cabal12.airnews.net!usenet
From: "John R. Strohm" <strohm@airmail.net>
Newsgroups: comp.lang.ada
Subject: Re: [Spark] Arrays of Strings
Date: Fri, 11 Apr 2003 08:14:05 -0500
Organization: Airnews.net! at Internet America
Message-ID: 
 <314749FA9ED0BA65.8D85E34D0ED0E4B0.A1DEBDFBF232880A@lp.airnews.net>
X-Orig-Message-ID: <b76fvp$9ug@library2.airnews.net>
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>
 <1050063540.619475@master.nyc.kbcfp.com>
Abuse-Reports-To: abuse at airmail.net to report improper postings
NNTP-Proxy-Relay: library2.airnews.net
NNTP-Posting-Time: Fri Apr 11 08:29:29 2003
NNTP-Posting-Host: ![l>?1k-WQkE6_> (Encoded at Airnews!)
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:36091
Date: 2003-04-11T08:14:05-05:00
List-Id: <comp.lang.ada>

"Hyman Rosen" <hyrosen@mail.com> wrote in message
news:1050063540.619475@master.nyc.kbcfp.com...
> 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.

Nope.

Declaring the types "snugly" is a good idea.  It gives more information to
the compiler and to the verification system.  It may OR MAY NOT make the
verification easier.
The point is that it is not mandatory: the verification system can figure
out the actual constraints.

Declaring the types "snugly" may make the verification harder.  Every time a
snugly-declared variable is assigned, a proof obligation is generated, to
prove that the variable will be in bounds.  Some of these obligations will
be trivial; some may not be.