Using Ada Contracts

Ada 2012 introduced contracts that provide a way to specify how a program should work.

Oct. 10, 2024

Ada 2012 introduced the idea of contracts. This TechXchange includes articles that delve into how they work and why contracts are useful. Contracts are also the basis for SPARK, a version of Ada that allows a program to be proven statically based on the contracts defined with a program.

More Articles About Ada/SPARK Contracts and Formal Verification

Ada 2012: The Joy of Contracts

The new Ada 2012 standard was recently approved by ISO. It incorporates contracts that will have a major impact on application design.

AdaCore

Contract-Driven Programming Takes Specification Beyond The Stone Age

The industrialization age of programming by contract is opening a new era in software development. Just as development techniques went from assembly to structured languages and...

AdaCore

Use Contracts To Enforce Effective Coding

From a software design point of view, contracts are a way of modeling requirements. They are a great foundation for safe programming and code correctness.

AdaCore

Q&A: Formal Methods Push Toward Zero-Defect Software

Technology Editor Bill Wong talks with AdaCore’s Yannick Moy about what formal verification of software brings to develop zero-defect software.

Requiem for a Bug – Verifying Software: Testing and Static Analysis

This article offers two approaches toward addressing the problem of software verification at increasing levels of sophistication.

AdaCore

Requiem for a Bug – Verifying Software, Part 2: Formal Verification through SPARK 2014

Formal verification, via tools like SPARK, can be used in a similar fashion to static analysis to find all run-time errors in your code, even the most unlikely of errors that ...

AdaCore