What is Correct-by-Construction software development?

Traditional approaches to software development rely on specifications written in English or another natural language, and hand-written program code. Sometimes a graphical notation such as UML is used to model the structure of the system and how it is used; but such models capture very little of the required behaviour, so that any code generated from them must be substantially reworked by hand. Either way, great reliance is placed on testing to uncover bugs in the software.

Correct-by-construction approaches treat software development as a true form of engineering. A civil engineer charged to build a bridge would construct an accurate computer model the proposed solution before laying the foundations. Similarly, a true software engineer constructs a mathematical model of his design before any code is produced. The model is used to reason about the proposed solution, ensuring that all required functionality will be delivered and the correct behavior exhibited. Testing is still performed, but its role is to validate the correct-by-construction process rather than to find bugs.

Perfect Developer is a unique model driven development tool that uses the verified design-by-contract paradigm for correct-by-construction software development.