The goal is to prevent errors from occurring in the first place.
This requires a mathematical proof of correctness for each piece of
code. Few programmers are trained in this technique. In addition, its results
to date, while very encouraging, seem to be about as good as one can do
with normal development followed by code inspection.
|Hall, A. ||Air Traffic Control system, developed using formal methods||
|Linger ||Cleanroom development. Metaanalysis of 17 projects with over 1 million LOC. Errors over life cycle||