Zero tolerance of defects
The principles of Correctness by Construction are:
- Don’t introduce errors in the first place.
- Remove any errors as close as possible to the point that they are introduced.
These are achieved by
- Using a sound, formal, notation for all deliverables. For example, use Z for writing software specifications, so it is impossible to be ambiguous. Code in SPARK, so it is impossible to introduce errors such as buffer overflow.
- Using strong, tool-supported methods to validate each deliverable. For example, carry out proofs of formal specifications and static analysis of code. This is only possible when using formal notations.
- Carrying out small steps and validating the deliverable from each step. For example, develop a software specification as an elaboration of the user requirements, and check that it is correct before writing code. Build the system in small increments, and check that each increment behaves correctly.
- Saying things only once. For example, produce a software specification, which says what the software will do, and a design, which says how it will be structured. The design should not repeat any information in the specification, and the two can be produced in parallel.
- Designing software that’s easy to validate. Write simple code that directly reflects the specification, and test it using tests derived systematically from that specification.
- Doing the hard things first. For example produce early prototypes to test out difficult design issues or key user interfaces.
As a result, Correctness by Construction is both effective and economical:
- Defects are removed early in the process when changes are cheap. Testing becomes a confirmation that the software works, rather than the point at which it must be debugged.
- Evidence needed for certification is produced naturally as a by-product of the process.
- Early iterations produce software that carries out useful functions and builds confidence in the project.