Correctness

Themes: Good software  

See the list of related resources at the bottom of this page.

When we say that a piece of software is correct, we mean that it does the right thing: in other words, it produces the right numbers, and exhibits the right behaviour. This is clearly a Good Thing, and is why correctness is one of the criteria for good software.

In order to tell whether a piece of software is correct, we must know what the right thing is; in other words, its behaviour must be specified. For calculations, this means stating the formulae and algorithms to be used; other behaviours must be described in similar rigorous terms. Behaviours that should be specified include:

  • Changes made to files
  • Changes made to databases
  • User dialogs that should appear
  • What constitutes a valid input
  • What should happen when an invalid input is encountered
  • What should happen when an error is encountered (eg, a file can't be found)
  • ...

The only way of telling whether software is in fact correct is by testing. And you can only test against the specification. So it is absolutely vital to specify your software as thoroughly as you can, and then to test it equally thoroughly.

Resources

Ray Panko
Professor Panko, who is at the University of Hawaii, has done a great deal of research into spreadsheet errors. His page at http://panko.cba.hawaii.edu/ssr/ has many useful resources, including links to many of his papers.
Is this spreadsheet a tax evader?
This paper, by Ray Butler of H.M. Customs and Excise, summarises the audit experience, describes the methodology and outlines the results to date of a campaign of spreadsheet testing started in July of 1999. Of the seven spreadsheets selected for audit, six contained significant errors. It was published in the proceedings of the 33rd Hawaii International Conference on System Sciences in 2000, and is available at http://www.eusprig.org/hicss33-butler-evader.pdf.
Managing the operational risks of user-developed software
This is a paper I wrote for a workshop at GIRO 2002. It is available from my publications page.