RE: (whimsy) Bug-free software

["David Crocker" <dcrocker () eschertech com>]

Alun Jones wrote:

> >
A user unable to understand the implementation detail would doubtless be
faced with a similar difficulty in understanding a requirements document
that is sufficiently detailed as to be used to generate a provably-correct
implementation.  It goes around and comes around.  At some point, a document
is produced that only a very few people could understand, and where all the
'coding' bugs are embodied.  Whether this is a formal requirement spec, or
source code, is of little matter.  You haven't got rid of the possibility of
bug, you've just moved their location.
<<

No, there are substantial differences. The requirements document will be
substantially shorter and much higher level than the implementation, and
therefore easier to digest.

For example, consider a requirement that "if the user presses the UNDO button,
the state of the document will be restored to the state prior to the previous
operation". Even though it will then be necessary to specify what is meant by
"the previous operation", this specification will certainly be substantially
shorter than the code needed to implement a multi "undo".

Or consider the requirement "The package will not crash no matter what input it
receives from the user and/or the Internet". This is very easy to state, but
will typically involve a large amount of code.

Assuming comparable notations, requirements statements are shorter then
specifications, and specifications are much shorter than code. So although
getting the requirements right is certainly not easy, it is much easier than
relying on manual means to get the requirements AND the specification AND the
implementation right.

Apart from this, mathematical methods frequently detect inconsistencies and
incompleteness in the requirements which are very hard to spot manually.

David Crocker
Escher Technologies Ltd.
www.eschertech.com
Tel. +44(0)1252 336565  Fax +44(0)1252 320954