Ada: Contracts

Since Ada 2012, subprograms and types can carry contracts: preconditions, postconditions, type invariants, and subtype predicates written as aspects in the specification. A contract is a promise the toolchain can check — at run time in Ada, and statically in SPARK, Ada's provable subset.

Pre- and Postconditions

Aspects attach to a declaration with with Aspect => expression. The precondition states what the caller must guarantee; the postcondition states what the body must deliver:

Contract checking flow: caller satisfies the precondition, callee establishes the postcondition
Fig. 1 — A violation localizes the bug: precondition failure is a caller bug; postcondition failure is a callee bug.
with Ada.Text_IO; use Ada.Text_IO;

procedure Contract_Demo is

   function Sqrt (X : Float) return Float
     with Pre  => X >= 0.0,                       -- caller's obligation
          Post => abs (Sqrt'Result ** 2 - X) < 1.0e-4   -- callee's obligation
   is
      R : Float := X;
   begin
      --  Newton's method: converges quadratically for X >= 0
      if X > 0.0 then
         for I in 1 .. 20 loop
            R := (R + X / R) / 2.0;
         end loop;
      end if;
      return R;
   end Sqrt;

begin
   Put_Line (Float'Image (Sqrt (9.0)));   -- 3.0
   --  Put_Line (Float'Image (Sqrt (-1.0)));
   --  ^ raises Assertion_Error at the CALL SITE: the caller broke the contract
end Contract_Demo;

The key property: failures localize. When a precondition fails, the bug is in the caller, not in Sqrt. When a postcondition fails, the bug is in the body. Debugging stops being "where did the wrong value come from" and becomes "which side of the boundary is broken."

Contracts in the Specification

On a package boundary the contract becomes part of the API every client compiles against — the documentation that cannot rot:

package Stack is
   subtype Capacity is Natural range 0 .. 128;

   type Stack is private
     with Type_Invariant => Valid (Stack);   -- every object, always

   procedure Push (S : in out Stack; Item : Integer)
     with Pre  => Length (S) < Capacity'Last,
          Post => Length (S) = Length (S'Old) + 1;

   function Length (S : Stack) return Capacity;
   function Valid (S : Stack) return Boolean;
private
   ...   -- the invariant keeps the internal state honest
end Stack;

S'Old refers to the parameter's value at entry — the standard way to state "after this call, X grew by one."

Subtype Predicates

Predicates generalize range constraints to any Boolean expression — a Dynamic_Predicate or, better, a Static_Predicate the compiler can often check statically:

procedure Predicate_Demo is
   subtype Even is Integer
     with Static_Predicate => Even mod 2 = 0;

   subtype Month_Name is String (1 .. 3)
     with Static_Predicate => Month_Name in
       "Jan" | "Feb" | "Mar" | "Apr" | "May" | "Jun" |
       "Jul" | "Aug" | "Sep" | "Oct" | "Nov" | "Dec";

   E : Even := 8;
begin
   --  E := 7;      -- Predicate check fails: Assertion_Error at the assignment
   null;
end Predicate_Demo;

Predicates apply in every context the subtype appears — parameters, aggregates, conversions — making them the cheapest possible validation layer.

A Taste of SPARK

SPARK is a subset of Ada (no access types except under rules, no side-effecting functions, restricted exceptions) plus a toolset (gnatprove) that proves contracts mathematically — no run-time checks, no test cases for the paths they cover:

package Math_Util with SPARK_Mode is
   function Increment (X : Natural) return Natural
     with Pre  => X < Natural'Last,
          Post => Increment'Result = X + 1;
   --  gnatprove proves: the postcondition holds for ALL inputs
   --  satisfying the precondition — no execution required.
end Math_Util;

The same annotation skills this chapter teaches are exactly what SPARK consumes. Industrial examples: SPARK-proven code runs in aircraft, the token-based secure systems world (e.g. verified crypto libraries like(Token)R and GNAT's own run-time subsets), and NASA's OS-based projects.

Next: Tasking — concurrency as a language construct.