Overview

Much has been written about why software is so defect prone and about why the problem of designing and writing software is so intrinsically difficult. Researchers recognize both the essential and accidental difficulties of producing correct software. Essential difficulties arise from the inherent challenge of understanding a complex application and operating environment, and from having to construct a structure comprising an extremely large number of states, with very complex state-transition rules. Further, software is subject to frequent modifications, as new features are added to adapt to changing application needs. In addition, as hardware and operating system platforms change with time, the software has to adjust appropriately. Finally, software is often used to paper over incompatibilities between interacting system components.

Accidental difficulties in producing good software arise from the fact that people make mistakes in even relatively simple tasks. Translating the detailed design into correctly working code may not require such advanced skills as creating a correct design in the first place but is also mistake prone.

A great deal of work has gone into techniques to reduce the defect rate of modern software. These techniques rely on extensive procedures to test software programs for correctness and completeness. Testing, however, can never conclusively verify the correctness of an arbitrary program. This can only be approached through a formal mathematical proof. Constructing such formal proofs is currently the subject of much active research; however, the state of the art at the present time is rather primitive, and formal program...