Safety-Critical & High-Integrity Ada
Apply Ada in certified domains: standards (DO-178C, EN 50128, ISO 26262, IEC 61508), pragma Restrictions and Profile (No_Allocators, No_Recursion, No_Exception_Handlers, Ravenscar, Jorvik), configuration files (gnat.adc), validity checking (Initialize_Scalars, Normalize_Scalars, -gnatVa), coding standards, static analysis, and the traceability mindset.
Ada's biggest users are systems where failure costs lives: aircraft, trains, medical devices, military and space systems. Certification standards demand evidence that software does what it should and nothing else. Ada supports this with language-level restrictions that remove hard-to-analyse features, validity checking, analysable tasking profiles, and tools that turn source code into certification evidence.
Standards and Why Ada Fits
DO-178C (avionics), EN 50128 / EN 50716 (railway), ISO 26262 (automotive), IEC 61508 (industrial) and IEC 62304 (medical) grade software by criticality and require requirements traceability, structural coverage (up to MC/DC), verification of absence of run-time errors and deterministic resource use. Ada's strong typing, explicit contracts, bounded tasking (Ravenscar) and SPARK proofs provide much of this evidence directly. Well-known uses include Boeing 777/787 avionics, Airbus systems, the Paris Métro line 14, air traffic control, and many satellites.
• DO-178C, EN 50128, ISO 26262, IEC 61508, IEC 62304. • Evidence: traceability, coverage, absence of RTE, bounded resources. • Ada + SPARK + Ravenscar supply much of it.
Restrictions, Profiles and Configuration
pragma Restrictions forbids language features program-wide, and the compiler/binder enforce them: No_Allocators (no heap), No_Recursion, No_Exception_Handlers, No_Floating_Point, No_Implicit_Heap_Allocations, No_Dispatch, Max_Tasks => 0, and many more. pragma Profile groups restrictions: Ravenscar, Jorvik, No_Implementation_Extensions, and GNAT's restricted runtimes (ZFP/light, light-tasking, embedded). Configuration pragmas typically live in a gnat.adc file (or the project's Global_Configuration_Pragmas) so they apply to every unit.
Validity: pragma Normalize_Scalars (standard) and Initialize_Scalars (GNAT) initialize otherwise uninitialized scalars with invalid values, so that reading them by mistake is detectable ('Valid, -gnatVa validity checks). Normalize_Scalars must be used for the whole partition including the runtime; in this course's toolchain the binder rejected it with 'some but not all files compiled with Normalize_Scalars', while Initialize_Scalars worked. Coding standards (e.g. GNATcheck rules, MISRA-like subsets), static analysers (CodePeer/GNAT SAS) and coverage tools (GNATcoverage) complete the toolbox.
• pragma Restrictions (...) and pragma Profile (...) in gnat.adc. • Normalize_Scalars (whole partition) / Initialize_Scalars (GNAT) + 'Valid, -gnatVa. • GNATcheck, GNAT SAS, GNATcoverage for evidence.
Code Examples
The gnat.adc configuration is picked up automatically by gnatmake. The program uses only static data, and Initialize_Scalars makes the uninitialized variable detectably invalid (GNAT also warns that Uninit is read but never assigned). Output: Average level = 52 Uninit'Valid = FALSE
The same restrictions reject heap allocation and recursion at compile time. Real GNAT diagnostics: l63_err.adb:3:04: warning: "P" is not modified, could be declared constant [-gnatwk] l63_err.adb:3:19: error: violation of restriction "No_Allocators" at gnat.adc:2 l63_err.adb:6:32: error: violation of restriction "No_Recursion" at gnat.adc:3 -- relying on reviews to find heap use in flight code pragma Restrictions (No_Allocators); -- enforced by the compiler
Machine-checked restrictions are cheaper and more reliable than manual review.
exception when others => null; -- in safety-critical code -- prove absence of exceptions (SPARK) or handle specific, analysed failure modes
Swallowing exceptions hides faults; certification needs defined failure behavior.
pragma Normalize_Scalars; -- in one unit only -- apply to the whole partition (including the runtime) or use GNAT's Initialize_Scalars
The binder requires consistency (verified error).
Which restriction forbids heap allocation? A. No_Heap B. No_Allocators C. No_Access D. Static_Only
Where are program-wide configuration pragmas usually placed with GNAT? A. In every unit B. In gnat.adc (or project Global_Configuration_Pragmas) C. In the main procedure only D. In a .c file
Which avionics standard governs airborne software? A. ISO 9001 B. DO-178C C. IEC 62304 D. EN 50128
What is the purpose of Normalize_Scalars / Initialize_Scalars? A. Speed B. Make uninitialized scalars detectably invalid C. Zero all memory D. Pack records Why is this rejected?
Real GNAT output: l63_err.adb:3:04: warning: "P" is not modified, could be declared constant [-gnatwk] l63_err.adb:3:19: error: violation of restriction "No_Allocators" at gnat.adc:2 l63_err.adb:6:32: error: violation of restriction "No_Recursion" at gnat.adc:3
-- file: gnat.adc
-- Configuration pragmas for the whole program (a high-integrity profile)
pragma Restrictions (No_Allocators); -- no heap allocation
pragma Restrictions (No_Recursion); -- bounded stack
pragma Restrictions (No_Floating_Point);
pragma Restrictions (Max_Tasks => 0);
pragma Initialize_Scalars; -- GNAT: uninitialized scalars get invalid values
-- file: l63_safety.adb
with Ada.Text_IO; use Ada.Text_IO;
procedure L63_Safety is
type Level is range 0 .. 100;
type Table is array (1 .. 5) of Level;
-- Static, bounded data; no pointers, no recursion, no heap
Readings : constant Table := [12, 55, 70, 33, 91];
Uninit : Level; -- deliberately not initialized
function Average (T : Table) return Level is
Sum : Integer := 0;
begin
for R of T loop
Sum := Sum + Integer (R);
end loop;
return Level (Sum / T'Length);
end Average;
begin
Put_Line ("Average level =" & Level'Image (Average (Readings)));
-- Initialize_Scalars sets Uninit to an invalid value where possible, so reading
-- it by mistake is detectable with 'Valid (and by validity checks, -gn
…-- file: gnat.adc
-- Configuration pragmas for the whole program (a high-integrity profile)
pragma Restrictions (No_Allocators); -- no heap allocation
pragma Restrictions (No_Recursion); -- bounded stack
pragma Restrictions (No_Floating_Point);
pragma Restrictions (Max_Tasks => 0);
pragma Initialize_Scalars; -- GNAT: uninitialized scalars get invalid values
-- file: l63_err.adb
procedure L63_Err is
type Int_Ptr is access Integer;
P : Int_Ptr := new Integer'(5); -- heap allocation
function Fact (N : Natural) return Natural is
(if N = 0 then 1 else N * Fact (N - 1)); -- recursion
begin
P.all := Fact (P.all);
end L63_Err;