SPARK is a subset of Ada (no access types in old versions, no side effects in functions, no exceptions handled) designed for formal proof. Enable it with pragma SPARK_Mode (On); or with SPARK_Mode.
Ada Expert · Lesson 1 · On the house
SPARK: provable Ada
SPARK_Mode, Global and Depends contracts, loop invariants, and what gnatprove proves. Lesson 1 is free — on the house.
Lessons · Ada Expert · Lesson 1 of 10 · On the house
SPARK: provable Ada
SPARK_Mode, Global and Depends contracts, loop invariants, and what gnatprove proves.
gnatprove proves absence of runtime errors (overflow, index, range) and that Pre/Post hold, all without running the code.
Global => (In_Out => Counter) declares exactly which globals a subprogram touches; Depends states data flow.
Loops need pragma Loop_Invariant (...) so the prover can reason about every iteration.
SPARK code is still Ada: GNAT compiles and runs it normally, as below.
SPARK contracts
pragma Assertion_Policy (Check);
with Ada.Text_IO; use Ada.Text_IO;
procedure Spark_Demo with SPARK_Mode is
type Index is range 1 .. 10;
type Arr is array (Index) of Natural;
Total : Natural := 0;
function Sum_Prefix (A : Arr; Last : Index) return Natural
with Pre => (for all I in Index => A (I) <= 1000),
Post => Sum_Prefix'Result <= 1000 * Natural (Last)
is
S : Natural := 0;
begin
for I in Index'First .. Last loop
S := S + A (I);
pragma Loop_Invariant (S <= 1000 * Natural (I));
end loop;
return S;
end Sum_Prefix;
procedure Add (X : Natural)
with Global => (In_Out => Total),
Pre => Total <= Natural'Last - X,
Post => Total = Total'Old + X
is
begin
Total := Total + X;
end Add;
Data : constant Arr := (others => 7);
begin
Add (Sum_Prefix (Data, 4));
Add (2);
Put_Line (Total'Image);
end Spark_Demo;
Quiz
Quiz
Quiz
Quiz
Check
Match the still for: SPARK: provable Ada.
Open-book: the answers are on this page. Pass every quiz and check (5) to mark the lesson done. This visit: 0/5.