This article series is in the Embedded Software topic within our Series Library
This article series is also in the TechXchange: Developing High Quality Software
Safe and secure software requires code to meet specifications. These are often written documents that have to be translated into applications by programmers. Unfortunately, the contract between the specifications and implementation can be tenuous and even ignored, which can lead to problems. It would be great if the specifications could be enforced by the compiler.
Contracts are a technology added to Ada 2012 and based on SPARK, a provable subset of Ada. A programmer can annotate aspects of the software, such as the pre- and post-conditions. This allows the compiler to prove that the code does what is specified by the developer. This includes code that may call a function, allowing many validity checks to be removed since the compiler makes sure arguments meet the specified requirements.
These articles provide examples and insights into contract-based programming:
- Ada 2012: The Joy of Contracts
- Contract-Driven Programming Takes Specification Beyond The Stone Age
- Use Contracts To Enforce Effective Coding
- Q&A: Formal Methods Push Toward Zero-Defect Software
- Requiem for a Bug – Verifying Software: Testing and Static Analysis
- Requiem for a Bug – Verifying Software, Part 2: Formal Verification through SPARK 2014
An Intro to Spark is another good resource. It is an interactive website where you can try out contracts.