We are modeling a safety-critical system using SPARK Ada, the system is a simple Rocket Control System. Here is the code, first for Rocket_Control_System.ads: pragma SPARK_Mode (On);

with SPARK.Text_IO;
use SPARK.Text_IO;

package Rocket_Control_System is

   Max_Current : constant Integer := 100;
   Critical_Current : constant Integer := 80;

   type Current_Range is new Integer range 0 .. Max_Current;

   type Rocket_Status_Type is (Valves_Opened, Self_Destruct);

   type Rocket_System_Status is
      record
         Measured_Current : Current_Range;
         Rocket_Status : Rocket_Status_Type;
      end record;

   Rocket_System : Rocket_System_Status;

   procedure Get_Current with
      Global => (In_Out => (Standard_Output, Standard_Input, Rocket_System)),
      Depends => (Standard_Output => (Standard_Output, Standard_Input),
                  Standard_Input  => Standard_Input,
                  Rocket_System   => (Rocket_System, Standard_Input));

   function Rocket_Status_To_String (Status : Rocket_Status_Type) return String;

   procedure Print_Status with
      Global => (In_Out => Standard_Output, Input => Rocket_System),
      Depends => (Standard_Output => (Standard_Output, Rocket_System));

   function Is_Safe (Status : Rocket_System_Status) return Boolean is
      (if Integer(Status.Measured_Current) > Critical_Current
         then Status.Rocket_Status = Self_Destruct
         else Status.Rocket_Status = Valves_Opened);

   procedure Monitor_Rocket_System with
      Global  => (In_Out => (Standard_Input, Standard_Output, Rocket_System)),
      Depends => ((Rocket_System, Standard_Input, Standard_Output) => (Rocket_System, Standard_Input, Standard_Output)),
      Post    => Is_Safe(Rocket_System);

   procedure Init_Rocket_System with
      Global => (Output => (Standard_Output, Standard_Input, Rocket_System)),
      Depends => ((Standard_Output, Standard_Input, Rocket_System) => null),
      Post    => Is_Safe(Rocket_System);

end Rocket_Control_System;
Secondly, Rocket_Control_System.adb: pragma SPARK_Mode (On);

with AS_IO_Wrapper;
use AS_IO_Wrapper;

package body Rocket_Control_System is


   procedure Get_Current is
      Current : Integer;
   begin
      AS_Put_Line("Enter sensor value in amps");
      loop
         AS_Get(Current, "Please type in an integer");
         exit when (Current >= 0) and (Current <= Max_Current);
         AS_Put("Please type in a value between 0 and ");
         AS_Put(Max_Current);
         AS_Put_Line("");
      end loop;
      Rocket_System.Measured_Current := Current_Range(Current);
   end Get_Current;


   function Rocket_Status_To_String (Status : Rocket_Status_Type) return String is
   begin
      if Status = Valves_Opened then
         return "Valves Opened";
      else
         return "Self Destruct";
      end if;
   end Rocket_Status_To_String;


   procedure Print_Status is
   begin
      AS_Put("Current = ");
      AS_Put(Integer(Rocket_System.Measured_Current));
      AS_Put_Line("");
      AS_Put("Rocket Control System = ");
      AS_Put_Line(Rocket_Status_To_String(Rocket_System.Rocket_Status));
   end Print_Status;


   procedure Monitor_Rocket_System is
   begin
      Get_Current;

      if Integer(Rocket_System.Measured_Current) > Critical_Current then
         Rocket_System.Rocket_Status := Self_Destruct;
      else
         Rocket_System.Rocket_Status := Valves_Opened;
      end if;

      Print_Status;
   end Monitor_Rocket_System;

   procedure Init_Rocket_System is
   begin
      AS_Init_Standard_Input;
      AS_Init_Standard_Output;
      Rocket_System := (Measured_Current => 0,
                        Rocket_Status => Valves_Opened);
   end Init_Rocket_System;

end Rocket_Control_System;
Thirdly, main.ads: Pragma SPARK_Mode (On);

procedure Main;
Fourthly, main.adb: pragma SPARK_Mode (On);
with Rocket_Control_system;
use Rocket_Control_system;

procedure Main
is
begin
   Init_Rocket_System;
   loop
      pragma Loop_Invariant (Is_Safe(Rocket_System));
      Get_Current;
      Monitor_Rocket_System;
      Print_Status;
   end loop;
end Main;