To edit the page, the password is go
taken from Correctness by Construction: A Manifesto for High-Integrity Software

Fundamental Principles

The primary goals of very low defect rate and very high resilience to change are realized in CbyC by two fundamental principles: to make it difficult to introduce errors in the first place, and to detect and remove any errors that do occur as early as possible after introduction.

The key to implementing these principles is to introduce sufficient precision at each step of the software development to enable reasoning about the correctness of that step – reasoning in the sense that an argument for correctness can be established either by review or using tool support. The aim is to demonstrate or argue the software correctness in terms of the manner in which it has been produced (by construction) rather than just by observing operational behavior.

It is the use of precision that differentiates approaches such as CbyC from others in common use. Typically, software development approaches endure a lack of precision that makes it very easy to introduce errors, and very hard to find those errors early. Evidence for this may be found in the common tendency for development life cycles to migrate to an oftenrepeating code-test-debug phase, which can lead to severe cost and timescale overruns.

Conversely, the rigor and precision of the CbyC approach means that the requirements are more likely to be correct, the system is more likely to be the correct system to meet the requirements, the implementation is more likely to be defect-free, and upgrades are more likely to retain the original correctness properties.

Achieving the Fundamental Principles

The principles of making it difficult to introduce defects and making it easy to detect and remove errors early are achieved by a combination of the following six strategies:

• Using a sound, formal notation for all deliverables. For example, using Z for writing specifications so it is impossible to be ambiguous, or using SPARK to write the code so it is impossible to introduce errors such as buffer overflows.
• Using strong, tool-supported methods to validate each deliverable. For example, carrying out proofs of formal specifications and static analysis of code. This is only possible where formal notations are used (strategy No. 1).
• Carrying out small steps and validating the deliverable from each step. For example, developing a software specification as an elaboration of the user requirements, and checking that it is correct before writing code. For example, building the system in small increments and checking that each increment behaves correctly.
• Saying things only once. For example, by producing a software specification that says what the software will do and a design that says how it will be structured. The design does not repeat any information in the specification, and the two can be produced in parallel.
• Designing software that is easy to validate. For example, writing simple code that directly reflects the specification, and testing it using tests derived systematically from that specification.
• Doing the hard things first. For example, by producing early prototypes to test out difficult design issues or key user interfaces.

These six principles are not in themselves difficult to apply, and may even appear obvious. However, in the authors’ experience, many software development projects fail to deliver against many, if any, of these principles.