SPARK: Formal Verification of Ada Programs
Understand SPARK — the formally verifiable subset of Ada — and its levels (stone, bronze, silver, gold, platinum), SPARK_Mode, data-flow contracts (Global, Depends), proof of absence of run-time errors, functional contracts, loop invariants and variants, ghost code, and how GNATprove is run.
SPARK is a subset of Ada designed for formal verification, plus contracts and a toolset (GNATprove) that proves properties mathematically — for all possible inputs, not just the ones you tested. It is used for avionics, security software (e.g. hypervisors and cryptography), and railway systems. Because SPARK is Ada, the same code compiles with GNAT and runs normally.
The SPARK Subset and Assurance Levels
'with SPARK_Mode' marks a unit as SPARK. The subset excludes features that defeat analysis: side effects in functions (except special cases), aliasing between parameters, exceptions handlers, goto, and unrestricted pointers (SPARK has an ownership model for access types, similar to Rust's borrowing). Adoption levels: Stone — valid SPARK; Bronze — correct data and information flow (no uninitialized reads); Silver — absence of run-time errors (no overflow, index or range failures); Gold — key functional properties proved; Platinum — full functional correctness.
• SPARK_Mode aspect; no side-effecting functions, aliasing, handlers. • Ownership model for pointers. • Levels: Stone → Bronze → Silver → Gold → Platinum.
Flow Contracts and Proof
Global states which global variables a subprogram reads or writes ('Global => null', 'Global => (In_Out => Total)'); Depends states which outputs depend on which inputs ('Depends => (A => (A, Lo, Hi))'). GNATprove's flow analysis checks these and detects uninitialized variables. Proof then generates verification conditions for every possible run-time check and every contract (Pre, Post, Loop_Invariant) and discharges them with automatic provers (Alt-Ergo, CVC5, Z3). A precondition like 'Total <= Integer'Last - X' is exactly what allows the prover to show Total + X cannot overflow.
• Global / Depends — data and information-flow contracts. • GNATprove proves run-time checks and contracts for all inputs. • Preconditions supply the facts needed to prove the body.
Loop Invariants, Variants and Ghost Code
Provers reason about loops through pragma Loop_Invariant — a property true at that point on every iteration, strong enough to imply the postcondition when the loop ends (in Find: no element before I equals Key). pragma Loop_Variant (Increases => X) proves termination. Ghost entities (with Ghost) exist only for specification: ghost variables, functions and lemmas are checked by the prover and removed from the executable when ghost code is disabled. When compiled with -gnata, GNAT executes contracts and invariants as run-time assertions — which is how this course runs the example; GNATprove itself is installed separately (e.g. 'alr install gnatprove') and was not part of the toolchain used here.
• pragma Loop_Invariant — per-iteration property used by the prover. • pragma Loop_Variant — termination argument. • Ghost code: specification-only, erasable. • With -gnata the same contracts run as assertions.
Code Examples
A SPARK package with flow contracts, functional postconditions and loop invariants, compiled by GNAT with -gnata so every contract and invariant was checked while running. Output of the executable: Find (Data, 13) = 3 Find (Data, 5) = 0 Clamped to 0 .. 50: 7 0 13 50 42 Total = 42
How GNATprove is typically invoked; it reports each check as proved or not proved, with counterexamples for failures.
procedure Add_To_Total (X: Integer); -- modifies global Total, no contract procedure Add_To_Total (X: Integer) with Global => (In_Out => Total), Pre =>..., Post => Total = Total'Old + X;
SPARK requires (or infers) Global; explicit contracts document and verify side effects.
for I in A'Range loop... -- no invariant; prover cannot conclude the postcondition pragma Loop_Invariant (for all J in A'First.. I - 1 => A (J) /= Key);
Loop invariants summarize what previous iterations established.
Total:= Total + X; -- unproved: possible overflow Pre => (if X > 0 then Total <= Integer'Last - X else Total >= Integer'First - X)
Silver level requires proving every overflow check; preconditions provide the bounds.
Which SPARK level proves absence of run-time errors? A. Stone B. Bronze C. Silver D. Platinum
What does 'Global => null' state? A. The subprogram is abstract B. It reads and writes no global variables C. It returns null D. It has no parameters
What is a loop invariant used for? A. Speeding up loops B. Stating a property that holds on every iteration so the prover can reason about the loop C. Unrolling D. Parallelizing
Can SPARK code be compiled by a normal Ada compiler? A. No B. Yes, SPARK is a subset of Ada C. Only with a plugin D. Only to C Trace the SPARK example.
Real output: Find (Data, 13) = 3 Find (Data, 5) = 0 Clamped to 0 .. 50: 7 0 13 50 42 Total = 42
Add a Loop_Variant to a binary search loop 'while Lo <= Hi loop'.
while Lo <= Hi loop pragma Loop_Invariant (Lo in A'Range and Hi < A'Last + 1); pragma Loop_Variant (Decreases => Hi - Lo); ... end loop;
Hi - Lo strictly decreases each iteration and is bounded, which proves termination.
-- file: search.ads
package Search
with SPARK_Mode -- this unit is written in the SPARK subset
is
type Int_Array is array (Positive range <>) of Integer;
Max_Updates : Natural := 0 with Ghost; -- ghost state: for specification only
function Contains (A : Int_Array; Key : Integer) return Boolean is
(for some E of A => E = Key);
function Find (A : Int_Array; Key : Integer) return Natural
with Global => null, -- reads/writes no globals
Post => (if Find'Result = 0 then not Contains (A, Key)
else Find'Result in A'Range and then A (Find'Result) = Key);
procedure Clamp_All (A : in out Int_Array; Lo, Hi : Integer)
with Global => null,
Depends => (A => (A, Lo, Hi)), -- information flow
Pre => Lo <= Hi,
Post => (for all I in A'Range => A (I) in Lo .. Hi);
Total : Integer := 0;
procedure Add_To_Total (X : Integer)
with Global => (In_Out => Total),
Pre => (if X > 0 then Total <= Integer'Last - X else Total >= Integer'First - X),
Post => Total = Total'Old + X;
end S
…alr install gnatprove # get the prover via Alire (not run in this course)
gnatprove -P project.gpr --level=2 --report=all
gnatprove -P project.gpr --mode=flow # Bronze: data and information flow only