Wutthichai Luemuang | Dreamstime.com

Enforced Coding Using Ada Contracts

May 12, 2021
This multipart article series examines how Ada contracts provide SPARK with the ability to prove software correctness.

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:

An Intro to Spark is another good resource. It is an interactive website where you can try out contracts. 

Sponsored Recommendations

What are the Important Considerations when Assessing Cobot Safety?

April 16, 2024
A review of the requirements of ISO/TS 15066 and how they fit in with ISO 10218-1 and 10218-2 a consideration the complexities of collaboration.

Wire & Cable Cutting Digi-Spool® Service

April 16, 2024
Explore DigiKey’s Digi-Spool® professional cutting service for efficient and precise wire and cable management. Custom-cut to your exact specifications for a variety of cable ...

DigiKey Factory Tomorrow Season 3: Sustainable Manufacturing

April 16, 2024
Industry 4.0 is helping manufacturers develop and integrate technologies such as AI, edge computing and connectivity for the factories of tomorrow. Learn more at DigiKey today...

Connectivity – The Backbone of Sustainable Automation

April 16, 2024
Advanced interfaces for signals, data, and electrical power are essential. They help save resources and costs when networking production equipment.