Re: [Spark] Arrays of Strings

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

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

Disclaimer: This is not a discussion of SPARK as such, but instead of formal
verification in the general sense.

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.

Consider

procedure main is
i:integer;
x: array(1..10) of real;
begin
  for i in 2..4 loop
    x(2*i+1) := 0;
  end loop;
end;

The array X is declared to be (1..10).  This generates an obligation that
for all X(<foo>), 1 le <foo> and <foo> le 10.

In this particular case, the verifier must satisfy

for all i:integer, i in 2..4
  --> (implies)
2*i+1 in 1..10

or

for all i:integer, i in 2..4
  -->
2*i in 0..9

or

i in 2..4
  -->
i in 0..4

which is trivially true if your verifier knows how to deal with this kind of
inequality processing.  (That capability has existed since the late 1970s.)
And even if your verifier doesn't understand inequality intervals, it can
exhaustively enumerate all values of i that satisfy the hypothesis and check
that they satisfy the conclusion.  (Some model checkers do that kind of
thing.)

What normally happens is that you will generate a proof obligation that you
may not be able to prove.  This is normal.  Usually, you can't DISPROVE a
proof obligation, you can only fail to find a proof for it.  (There exist
mechanical procedures for finding proofs of theorems, that WILL succeed if a
proof does in fact exist.  They may take a while.)  There are typically two
reasons for this: 1) you haven't brought enough information into context, 2)
you've uncovered a bug.  (There is a third possibility: you've uncovered an
instance of Godel's Theorem, but in practice that doesn't seem to happen.)

Consider

procedure main is
i:integer;
x: array(1..10) of real;
begin
  for i in 2..4 loop
    x(2*i+3) := 0;
  end loop;
end;

The proof obligation will become

i in 2..4 --> 2*i+3 in 1..10
i in 2..4 --> 2*i in -2..7
i in 2..4 --> i in -1..3   *TILT*

At this point, your theorem prover will do something roughly analogous to
throwing up its hands and saying "Beats me, daddy-O".  (With apologies to
Maynard G. Krebs...)  You are expected to look at the problem, look at the
code, and say "DOH!" and fix the obvious error.

Yes, it would be a bit more self-documenting if i were declared to be
integer(1..10), but it doesn't actually matter for verification.

OK, but what if the subscript is coming from somewhere else?

Simple.  Consider

procedure foo(i:integer) is
x:array(1..10) of real;
begin
  x(i) := 42;
end;

Again, a proof obligation is generated, to prove that i is in 1..10.  The
proof obligation must then be propagated to all of the callers of foo, and
proved individually.  Whether that obligation is propagated automatically by
the verification environment, or manually by the programmer adding an entry
specification annotation, is implementation-dependent.  Obviously, either
way will work.

Made-up example:

procedure foo(i:integer) is
x:array(1..10) of real;
entryspec i in 1..10;
begin
  x(i) := 42;
end;

The use of an entry specification generally simplifies the verification of
foo, in that it tells the verifier what it is allowed to assume.  At the
same time, it explicitly generates a proof obligation on the callers of foo.