Re: Ada.Strings.Bounded

[Eric Hughes <eric.eh9@gmail.com>]

On Apr 14, 12:13 pm, Georg Bauhaus <rm.tsoh.plus-
bug.bauh...@maps.futureapps.de> wrote:
> It might be worth noting that this kind of "correctness"
> specifically precludes factors that are essential to typical
> Ada programming: for a program to solve a problem correctly,
> use of time and storage must stay within specified bounds, too.
>
> Is there a definition of "correctness" that includes more than
> the necessary, static, computer agnostic precondition
> of "left side of equation equals right side of equation" no
> matter when and how?

Yes.

To me, the quickest way of getting at the essence of such conditions
is to start trying to write them down.  You need symbols for that.
You need a function symbol for, say, the time something takes and
another for the space something takes.  You need units of time and
units of space for the results.  You need literal expressions for
durations of time and amounts of space to write down bounds.  All
these are analytical symbols that need not be part of the language
they are analyzing.

The traditional method of correctness uses only the symbols of a
programming language combined with those of predicate calculus.
Simply from lack of expressibility, this traditional method cannot
directly address issues of time and space.  You need to obtain those
symbols from somewhere, and this pretty much means constructing an
execution model that provides a place to root those symbols.
Execution models, however, are properties of the target processor and
execution environment, and thus outside of and, really, independent of
the abstractions of high-level languages.  So, to ground this in Ada,
should there be a Ada-wide execution model?  Probably not.  Might
there be someday a way of expressing an execution model in Ada?  I
would hope so.

One of the consequences of this is that, in general, you can't prove
performance predicates about a program by itself, but only together
with an execution model.  Admittedly most execution models are
similar, but it would be a error of categories to assert a universal
one. (I don't mean to say that a canonical one might not be useful.)
There's a whole area of practical experience to gather about the
similarities of such proof prior to standardization, and I wouldn't
rush in quickly.

Finally, in order for this to work, you have to be able to connect
execution of the high-level program with execution of a program of
equivalent effect in the execution model.  This is where that Hoare
paper that I mentioned a while back, "Proof of correctness of data
representations" comes in.  It describes exactly how this works.

Eric