Contracts: Preconditions & Postconditions
Specify subprogram contracts with Pre and Post aspects, use 'Old and 'Result, write contracts with quantified and conditional expressions, understand who is to blame for a failure, how contracts are checked (Assertion_Policy, -gnata), and how they become proof obligations in SPARK.
Design by contract is built into Ada 2012. A precondition (Pre) states what must be true when a subprogram is called — the caller's obligation. A postcondition (Post) states what the subprogram guarantees on return — the implementer's obligation. Contracts are executable documentation: they are checked at run time when enabled, and SPARK tools can prove them statically.
Pre and Post
Contracts are aspects on the subprogram declaration: 'procedure Increment (X : in out Integer; By : Positive) with Pre => X <= Integer'Last - By, Post => X = X'Old + By;'. Pre is evaluated on entry, Post on normal return. A failing Pre means the caller has a bug; a failing Post means the implementation has a bug — the exception message names which one and where ('failed precondition from file:line'). Contracts go on the declaration (spec), so clients see them.
• with Pre => ..., Post => ... on the declaration. • Failed Pre → caller's bug; failed Post → callee's bug. • Raised as Ada.Assertions.Assertion_Error when checks are enabled.
'Old, 'Result and Expressive Contracts
X'Old in a postcondition denotes the value of X on entry (the compiler saves a copy). F'Result denotes a function's return value. Contracts may use any Boolean expression: quantified expressions ('for all I in ... =>'), conditional expressions ('if Result /= 0 then A (Result) = Key'), membership tests, delta aggregates ('P = P'Old with delta X => 0') and calls to expression functions such as Is_Sorted, which name concepts and keep contracts readable. Contracts should not have side effects.
• X'Old — entry value; F'Result — returned value. • Use quantified/conditional expressions and helper expression functions. • Contracts must be side-effect free.
Enabling and Proving
Contracts are checked when the assertion policy is Check: GNAT's -gnata switch or pragma Assertion_Policy (Pre => Check, Post => Ignore) per kind. Many projects keep preconditions on in production (they guard against misuse) and postconditions on in testing. In SPARK, the same contracts become proof obligations: the prover shows statically that every call satisfies Pre and every body establishes Post, so the run-time checks can never fail. GNAT also supports Contract_Cases for listing disjoint input cases with their own postconditions.
• -gnata or pragma Assertion_Policy controls checking. • Pre in production, Post in testing is a common policy. • SPARK proves contracts statically; Contract_Cases for case-based specs.
Code Examples
Integer_Sqrt's postcondition fully specifies the result (7² ≤ 50 < 8²). The two caller bugs violate Increment's and Binary_Search's preconditions; the buggy Abs_Value violates its own postcondition. Messages identify the contract's source line. Output: Integer_Sqrt (50) = 7 Count = 15 Binary_Search (Sorted, 7) = 4 Caller bug -> failed precondition from l43_prepost.adb:23 Caller bug -> failed precondition from l43_prepost.adb:35 Callee bug -> failed postcondition from l43_prepost.adb:60 procedure Pop (S: in out Stack; E: out Item); -- body: if Is_Empty (S) then raise...
procedure Pop (S : in out Stack; E : out Item) with Pre => not Is_Empty (S);
State the requirement in the spec where callers see it (and tools can check it).
Post => Count = Count + 1 Post => Count = Count'Old + 1 Use 'Old to refer to the value on entry.
with Pre => Log_Call and then X > 0 -- Log_Call has side effects with Pre => X > 0
Contracts may be disabled; they must not change program state.
A precondition fails. Whose bug is it? A. The subprogram's B. The caller's C. The compiler's D. The runtime's B. The caller's.
What does X'Old denote in a postcondition? A. The previous version of the program B. The value of X on entry to the subprogram C. X's default value D. A deprecated attribute
How do you refer to a function's result in its postcondition? A. Result B. F'Result C. return D. F.Result
What does a failed contract check raise? A. Constraint_Error B. Ada.Assertions.Assertion_Error C. Contract_Error D. Program_Error
B. (verified messages: 'failed precondition from...') Trace the contract example.
Real output: Integer_Sqrt (50) = 7 Count = 15 Binary_Search (Sorted, 7) = 4 Caller bug -> failed precondition from l43_prepost.adb:23 Caller bug -> failed precondition from l43_prepost.adb:35 Callee bug -> failed postcondition from l43_prepost.adb:60
Write the contract for a function Max_Index (A : Int_Array) return Positive that returns the index of a maximum element.
function Max_Index (A : Int_Array) return Positive with Pre => A'Length > 0, Post => Max_Index'Result in A'Range and then (for all I in A'Range => A (I) <= A (Max_Index'Result));
The precondition rules out empty arrays; the postcondition says the result is a valid index whose element is ≥ every element.
with Ada.Text_IO; use Ada.Text_IO;
with Ada.Exceptions; use Ada.Exceptions;
with Ada.Assertions;
procedure L43_Prepost is
type Int_Array is array (Positive range <>) of Integer;
-- Preconditions state the caller's obligations; postconditions the callee's promises
function Integer_Sqrt (N : Natural) return Natural
with Post => Integer_Sqrt'Result ** 2 <= N
and then (Integer_Sqrt'Result + 1) ** 2 > N;
function Integer_Sqrt (N : Natural) return Natural is
R : Natural := 0;
begin
while (R + 1) ** 2 <= N loop
R := R + 1;
end loop;
return R;
end Integer_Sqrt;
procedure Increment (X : in out Integer; By : Positive)
with Pre => X <= Integer'Last - By,
Post => X = X'Old + By; -- 'Old: value on entry
procedure Increment (X : in out Integer; By : Positive) is
begin
X := X + By;
end Increment;
function Is_Sorted (A : Int_Array) return Boolean is
(for all I in A'First .. A'Last - 1 => A (I) <= A (I + 1));
function Binary_Search (A : Int_Array; Key : Integer) return Natural
with Pre => Is_Sorted (A),
Post => (if Binary_Search'Result
…