Re: Problems with proofs

[dewar@cs.nyu.edu (Robert Dewar)]

A more pragmatic note on proof of correctness and a real life example where
it could be used.

Yesterday, we got a most amazing GNAT bug report

   type signed_31 is range -2**30 .. +2**30-1;
   for signed'size use 31;

didn't work, GNAT wanted 32 bits, yet this was one entry in a huge table
with all possible sizes, and all the others worked fine.

Investigation showed a definite bug in the universal integer add routine,
it gave wrong results for very specific input.

Now here is a really good example of where POC would be useful. The spec
of the universal integer package is particularly well defined and simple
at a mathematical level, since integers are really easy to talk about
formally, even if their implementation is tricky!

So, we can easily write the spec.

Now, could we actually do the proof. Well first of all, we have to confine
ourselves to a very simple subset, but I think we pretty much meet this,
for example, I think this particular unit (Uintp in file uintp.ads/adb)
is pretty much in the Praxis SPARK subset, for which a formal definition
exists. 

You would have to hide one external interface, namely the access to the
dynamically expanded tables (we don't want to get into storage allocation
issues I think!)

It would still be a VERY difficult business to prove. In particular, the
proof of Knuth's Algorithm D for multi-precision division is definitely
very hard. I would guess that this is right at the edge of the state of
the art (I will ask a friend at Praxis what he thinks).

But, if we had put the effort in, a POC of uintp would certainly have
found this error, or rather made it impossible to prove that the code
was correct.

Of course you have to ask, is it worth it? And that's a tough one, proof
of correctness techniqes at any level can get VERY expensive, which is
why they are usually associated with high assurance code, where bugs
are very costly, such as safety critical code.