Re: [Spark] Arrays of Strings

["John R. Strohm" <strohm@airmail.net>]

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