Ada Handbook

with Ada.Text_IO; use Ada.Text_IO;

procedure Variables_Demo is
   -- Variable declaration: Name : Type := Initial_Value;
   X        : Integer := 42;
   Y        : Float   := 3.14;
   Flag     : Boolean := True;
   Ch       : Character := 'A';

   -- Constants: value fixed at compile time
   Max_Size : constant Integer := 100;
   Pi       : constant Float   := 3.14159265;

   -- No initializer -- value is undefined until assigned
   Count    : Integer;

   -- Multiple declarations of the same type
   A, B, C  : Integer := 0;

   -- Numeric literals: underscores allowed for readability
   Big_Num  : Integer := 1_000_000;
   Hex_Lit  : Integer := 16#FF_00#;   -- base#value# notation
   Bin_Lit  : Integer := 2#1010_1010#;

begin
   Count := 0;
   X := X + 1;        -- 43
   Put_Line (Integer'Image (X));   -- 'Image attribute: Integer -> String
end Variables_Demo;

-- Ada is strongly typed: every object has exactly one type.
-- Predefined scalar types from Standard:
--   Integer, Long_Integer, Short_Integer
--   Float, Long_Float, Short_Float
--   Boolean, Character, Wide_Character
--   String (array of Character)

-- User-defined enumeration type
type Day is (Mon, Tue, Wed, Thu, Fri, Sat, Sun);
Today : Day := Wed;

-- Integer type with explicit range
type Age_Type is range 0 .. 150;
My_Age : Age_Type := 30;

-- Floating-point type (digits = decimal precision)
type Angle is digits 10;
Theta : Angle := 1.5708;

-- Fixed-point type: delta = resolution, range bounds
type Voltage is delta 0.001 range -100.0 .. 100.0;
V : Voltage := 3.300;

-- Modular (unsigned, wraps around)
type Byte is mod 256;
B : Byte := 255;
B := B + 1;   -- wraps to 0

-- Record type
type Point is record
   X : Float := 0.0;
   Y : Float := 0.0;
end record;
P : Point := (X => 1.0, Y => 2.0);

-- Access type (pointer)
type Int_Ptr is access Integer;
Ptr : Int_Ptr := new Integer'(42);

-- Subtype: constrained view of a parent type, same operations
subtype Positive is Integer range 1 .. Integer'Last;
subtype Natural  is Integer range 0 .. Integer'Last;

subtype Teen_Age is Integer range 13 .. 19;
My_Teen : Teen_Age := 16;   -- checked at run time (Constraint_Error if violated)

-- Derived type: new type, incompatible with parent
type Meters is new Float;
type Seconds is new Float;

M : Meters  := 10.0;
S : Seconds := 5.0;
-- M := S;   -- ILLEGAL: different types prevent unit confusion

-- Subtype of an enumeration
type Day is (Mon, Tue, Wed, Thu, Fri, Sat, Sun);
subtype Weekday  is Day range Mon .. Fri;
subtype Weekend  is Day range Sat .. Sun;

-- Subtype with unconstrained array
type String is array (Positive range <>) of Character;   -- Standard definition
subtype Name_String is String (1 .. 20);

-- Subtype renaming (alias-like convenience)
subtype Index is Integer range 1 .. 1000;

-- Arithmetic
A := 10 + 3;    -- 13
A := 10 - 3;    -- 7
A := 10 * 3;    -- 30
A := 10 / 3;    -- 3  (integer division, truncates toward zero)
A := 10 mod 3;  -- 1  (mod: result has sign of right operand)
A := 10 rem 3;  -- 1  (rem: result has sign of left operand)
A := 2 ** 10;   -- 1024 (exponentiation)

-- Floating-point: same operators, true division
F := 10.0 / 3.0;  -- 3.3333...
F := abs (-5.0);  -- 5.0 (abs is a unary operator)

-- Relational  (return Boolean)
B := (3 = 3);    -- True    (= not ==)
B := (3 /= 4);   -- True    (/= not !=)
B := (3 < 4);    -- True
B := (3 <= 3);   -- True
B := (3 > 2);    -- True
B := (3 >= 3);   -- True

-- Logical (Boolean)
B := True and False;  -- False   (evaluates both operands)
B := True or  False;  -- True
B := True xor True;   -- False
B := not True;        -- False

-- Short-circuit logical operators
B := Cond1 and then Cond2;  -- Cond2 skipped if Cond1 is False
B := Cond1 or else  Cond2;  -- Cond2 skipped if Cond1 is True

-- String concatenation
S := 'Hello' & ', ' & 'World!';   -- 'Hello, World!'

-- if / elsif / else
if X > 0 then
   Put_Line ('positive');
elsif X < 0 then
   Put_Line ('negative');
else
   Put_Line ('zero');
end if;

-- case statement (all values must be covered, or use others)
type Day is (Mon, Tue, Wed, Thu, Fri, Sat, Sun);
case Today is
   when Mon | Tue | Wed | Thu | Fri => Put_Line ('Weekday');
   when Sat | Sun                   => Put_Line ('Weekend');
end case;

case Code is
   when 200       => Put_Line ('OK');
   when 404       => Put_Line ('Not Found');
   when 500 .. 599 => Put_Line ('Server Error');
   when others    => Put_Line ('Unknown');
end case;

-- Basic loop (infinite -- exit to break out)
loop
   N := N + 1;
   exit when N >= 10;
end loop;

-- while loop
while N < 10 loop
   N := N + 1;
end loop;

-- for loop (range is inclusive on both ends)
for I in 1 .. 10 loop
   Put (Integer'Image (I));
end loop;

-- for loop over enumeration
for D in Day loop
   Put_Line (Day'Image (D));
end loop;

-- Reverse iteration
for I in reverse 1 .. 10 loop
   Put (Integer'Image (I));
end loop;

-- Named loop and exit
Outer : for I in 1 .. 5 loop
   Inner : for J in 1 .. 5 loop
      exit Outer when I + J > 6;  -- exit named outer loop
   end loop Inner;
end loop Outer;

-- Procedure declaration (no return value)
procedure Swap (A, B : in out Integer) is
   Temp : Integer;
begin
   Temp := A;
   A    := B;
   B    := Temp;
end Swap;

-- Parameter modes:
--   in     : read-only input (default if mode omitted)
--   out    : write-only output (uninitialized on entry)
--   in out : read-write parameter

procedure Read_And_Print (Prompt : in String; Result : out Integer) is
begin
   Put (Prompt);
   Get (Result);
end Read_And_Print;

procedure Increment (X : in out Integer; By : in Integer := 1) is
begin
   X := X + By;
end Increment;

-- Calling procedures
declare
   A : Integer := 10;
   B : Integer := 20;
   R : Integer;
begin
   Swap (A, B);              -- A=20, B=10
   Increment (A);            -- A=21 (default By=1)
   Increment (A, By => 5);  -- named parameter, A=26
   Read_And_Print ('Enter: ', R);
end;

-- Procedure forward declaration (in package spec)
procedure Do_Work (Data : in out Integer);
-- Body in package body or later in same unit

-- Function must return a value; all paths must reach a return
function Add (A, B : Integer) return Integer is
begin
   return A + B;
end Add;

-- Expression function (Ada 2012) -- single expression body
function Square (X : Integer) return Integer is (X * X);
function Max (A, B : Integer) return Integer is (if A > B then A else B);

-- Function with local declarations
function Factorial (N : Natural) return Natural is
   Result : Natural := 1;
begin
   for I in 2 .. N loop
      Result := Result * I;
   end loop;
   return Result;
end Factorial;

-- Pure function (no side effects, no global state reads)
-- Marked with pragma Pure or aspect Pure => True
function Is_Prime (N : Natural) return Boolean
   with Pure
is
begin
   if N < 2 then return False; end if;
   for I in 2 .. N / 2 loop
      if N mod I = 0 then return False; end if;
   end loop;
   return True;
end Is_Prime;

-- Overloaded functions (same name, different parameter profiles)
function Convert (X : Integer) return Float is (Float (X));
function Convert (X : Float) return Integer is (Integer (X));

-- Recursive function
function Fib (N : Natural) return Natural is
begin
   if N <= 1 then return N; end if;
   return Fib (N - 1) + Fib (N - 2);
end Fib;

-- Package specification: the public interface (math.ads)
package Math is
   Pi : constant Float := 3.14159265;

   function Circle_Area (Radius : Float) return Float;
   function Hypotenuse  (A, B  : Float) return Float;

private
   -- Private section: visible to body, hidden from clients
   Epsilon : constant Float := 1.0e-7;
end Math;

-- Package body: implementation (math.adb)
with Ada.Numerics.Elementary_Functions; use Ada.Numerics.Elementary_Functions;

package body Math is
   function Circle_Area (Radius : Float) return Float is
   begin
      return Pi * Radius * Radius;
   end Circle_Area;

   function Hypotenuse (A, B : Float) return Float is
   begin
      return Sqrt (A * A + B * B);
   end Hypotenuse;
end Math;

-- Using a package
with Math;
with Ada.Text_IO; use Ada.Text_IO;

procedure Main is
begin
   Put_Line (Float'Image (Math.Circle_Area (5.0)));  -- qualified name
end Main;

-- Package instantiation (from generic)
with Ada.Text_IO;
package Int_IO is new Ada.Text_IO.Integer_IO (Integer);
-- now: Int_IO.Put (42);

-- Array type: constrained (fixed bounds)
type Int_Array is array (1 .. 10) of Integer;
A : Int_Array := (1, 2, 3, 4, 5, 6, 7, 8, 9, 10);

-- Aggregate with named association
B : Int_Array := (1 => 100, 2 => 200, others => 0);

-- Unconstrained array type (bounds specified at object creation)
type Vector is array (Integer range <>) of Float;
V : Vector (1 .. 5) := (1.0, 2.0, 3.0, 4.0, 5.0);

-- Multi-dimensional array
type Matrix is array (1 .. 3, 1 .. 3) of Float;
M : Matrix := ((1.0, 0.0, 0.0),
               (0.0, 1.0, 0.0),
               (0.0, 0.0, 1.0));

-- Array attributes
N   : Integer := A'Length;         -- 10: number of elements
Lo  : Integer := A'First;          -- 1:  lower bound
Hi  : Integer := A'Last;           -- 10: upper bound
Len : Integer := V'Length;         -- 5

-- Iterating with attribute-based bounds (portable)
for I in A'Range loop
   A (I) := A (I) * 2;
end loop;

-- Array slices (subarray view, same type)
Sub : Int_Array (1 .. 3) := A (1 .. 3);   -- slice

-- String is array (Positive range <>) of Character
S : String (1 .. 5) := 'Hello';
C : Character := S (1);   -- 'H'

-- Dynamic array via unconstrained with heap allocation
type Dyn_Arr is array (Positive range <>) of Integer;
type Dyn_Ptr is access Dyn_Arr;
P : Dyn_Ptr := new Dyn_Arr (1 .. 100);

-- Basic record
type Point is record
   X : Float := 0.0;
   Y : Float := 0.0;
end record;

P : Point := (X => 3.0, Y => 4.0);
P.X := 1.0;   -- field access

-- Record with mixed types
type Person is record
   Name : String (1 .. 30);
   Age  : Natural;
   Score: Float := 0.0;
end record;

-- Discriminant: a parameter that determines the record's structure
type Dynamic_String (Length : Natural) is record
   Data : String (1 .. Length);
end record;
DS : Dynamic_String (10) := (Length => 10, Data => 'Hello     ');

-- Variant record: discriminant selects which fields exist
type Shape_Kind is (Circle, Rectangle, Triangle);

type Shape (Kind : Shape_Kind) is record
   case Kind is
      when Circle =>
         Radius : Float;
      when Rectangle =>
         Width, Height : Float;
      when Triangle =>
         Base, Height_T : Float;
   end case;
end record;

C : Shape := (Kind => Circle, Radius => 5.0);
R : Shape := (Kind => Rectangle, Width => 3.0, Height => 4.0);

-- Record aggregate (positional)
P2 : Point := (1.0, 2.0);

-- Record aggregate (named -- preferred for clarity)
P3 : Point := (X => 1.0, Y => 2.0);

with Ada.Unchecked_Deallocation;

procedure Access_Demo is
   -- Named access type
   type Int_Ptr is access Integer;

   -- Allocate with new; 'initialize with tick notation
   P : Int_Ptr := new Integer'(42);
   Q : Int_Ptr := new Integer;   -- uninitialized

   -- Access to record
   type Node;
   type Node_Ptr is access Node;
   type Node is record
      Value : Integer;
      Next  : Node_Ptr := null;
   end record;

   Head : Node_Ptr := new Node'(Value => 1, Next => null);

   -- Deallocation procedure (instantiate Unchecked_Deallocation)
   procedure Free is new Ada.Unchecked_Deallocation (Integer, Int_Ptr);
   procedure Free_Node is new Ada.Unchecked_Deallocation (Node, Node_Ptr);

   -- Access parameter (anonymous access -- no need to declare a type)
   procedure Print_Val (Ptr : access Integer) is
   begin
      if Ptr /= null then
         Ada.Text_IO.Put_Line (Integer'Image (Ptr.all));
      end if;
   end Print_Val;

begin
   P.all := 99;          -- dereference with .all
   Q.all := P.all + 1;   -- 100

   Print_Val (P);        -- anonymous access argument

   -- Build a simple linked list
   Head.Next := new Node'(Value => 2, Next => null);

   -- Free memory (sets pointer to null)
   Free (P);   -- P is now null
   Free (Q);

   -- null check
   if Head = null then
      Ada.Text_IO.Put_Line ('empty');
   end if;
end Access_Demo;

with Ada.Text_IO;          use Ada.Text_IO;
with Ada.Exceptions;       use Ada.Exceptions;

procedure Exception_Demo is
   -- Predefined exceptions (from Standard / Ada.IO_Exceptions etc.)
   --   Constraint_Error  -- range violation, null dereference, index out of bounds
   --   Program_Error     -- improper use of language features
   --   Storage_Error     -- heap exhausted
   --   Tasking_Error     -- task communication failure

   -- User-defined exception
   Invalid_Input : exception;
   Network_Error : exception;

   procedure Validate (X : Integer) is
   begin
      if X < 0 then
         raise Invalid_Input with 'Value must be non-negative: ' & Integer'Image (X);
      end if;
   end Validate;

begin
   -- Basic exception handler
   begin
      Validate (-5);
   exception
      when Invalid_Input =>
         Put_Line ('Caught: invalid input');
      when Constraint_Error =>
         Put_Line ('Caught: constraint error');
      when E : others =>
         -- E is the exception occurrence; use Ada.Exceptions to inspect it
         Put_Line ('Unexpected: ' & Exception_Name (E));
         Put_Line ('Message   : ' & Exception_Message (E));
   end;

   -- Re-raise in a handler
   begin
      Validate (-1);
   exception
      when Invalid_Input =>
         Put_Line ('Logging error...');
         raise;   -- re-raise the same exception
   end;

   -- Exception in a function: propagates to caller
   declare
      Result : Integer;
   begin
      Result := 10 / 0;   -- raises Constraint_Error
   exception
      when Constraint_Error => Put_Line ('Division by zero');
   end;
end Exception_Demo;

-- Generic subprogram
generic
   type Element_Type is private;       -- any type with assignment and equality
procedure Swap (A, B : in out Element_Type);

procedure Swap (A, B : in out Element_Type) is
   Temp : Element_Type;
begin
   Temp := A;
   A    := B;
   B    := Temp;
end Swap;

-- Instantiate the generic
procedure Swap_Int is new Swap (Integer);
procedure Swap_Flt is new Swap (Float);

-- Generic package
generic
   type Key_Type   is private;
   type Value_Type is private;
   with function '<' (L, R : Key_Type) return Boolean is <>;   -- formal function
package Ordered_Map is
   type Map is private;
   procedure Insert (M : in out Map; K : Key_Type; V : Value_Type);
   function  Find   (M : Map; K : Key_Type) return Value_Type;
private
   -- ... implementation details
end Ordered_Map;

-- Generic with type constraints
generic
   type Num is digits <>;   -- any floating-point type
package Statistics is
   function Mean     (Data : array (Integer range <>) of Num) return Num;
   function Variance (Data : array (Integer range <>) of Num) return Num;
end Statistics;

-- Instantiation
package Float_Stats is new Statistics (Float);
package Long_Stats  is new Statistics (Long_Float);

-- Instantiate standard containers
with Ada.Containers.Vectors;
package Int_Vectors is new Ada.Containers.Vectors
   (Index_Type   => Natural,
    Element_Type => Integer);

with Ada.Text_IO; use Ada.Text_IO;

procedure Tasking_Demo is

   -- Task type declaration
   task type Worker is
      entry Start (N : in Integer);   -- entry = synchronization point
      entry Get_Result (R : out Integer);
   end Worker;

   task body Worker is
      Input, Output : Integer;
   begin
      accept Start (N : in Integer) do   -- rendezvous: caller blocks until here
         Input := N;
      end Start;
      Output := Input * Input;   -- do work
      accept Get_Result (R : out Integer) do
         R := Output;
      end Get_Result;
   end Worker;

   -- Protected object: safe shared state (monitor-like)
   protected type Shared_Counter is
      procedure Increment;
      function  Value return Integer;
   private
      Count : Integer := 0;
   end Shared_Counter;

   protected body Shared_Counter is
      procedure Increment is begin Count := Count + 1; end Increment;
      function  Value return Integer is (Count);
   end Shared_Counter;

   W      : Worker;
   Result : Integer;
   Ctr    : Shared_Counter;

begin
   W.Start (7);                 -- initiate rendezvous
   W.Get_Result (Result);       -- wait for result
   Put_Line ('7^2 = ' & Integer'Image (Result));

   Ctr.Increment;
   Ctr.Increment;
   Put_Line ('Count = ' & Integer'Image (Ctr.Value));   -- 2
end Tasking_Demo;

-- Child packages extend a parent package's namespace.
-- Parent package: geometry.ads
package Geometry is
   type Point is record X, Y : Float; end record;
   function Distance (P, Q : Point) return Float;
end Geometry;

-- Public child: geometry-shapes.ads
-- Inherits visibility of Geometry's public declarations
package Geometry.Shapes is
   type Circle is record
      Center : Point;
      Radius : Float;
   end record;
   function Area      (C : Circle) return Float;
   function Perimeter (C : Circle) return Float;
end Geometry.Shapes;

-- Private child: geometry-internal.ads
-- Visible only within the Geometry hierarchy (not to external clients)
private package Geometry.Internal is
   function Approx_Equal (A, B : Float) return Boolean;
end Geometry.Internal;

-- Grandchild: geometry-shapes-svg.ads
package Geometry.Shapes.SVG is
   function To_SVG (C : Circle) return String;
end Geometry.Shapes.SVG;

-- Accessing child packages
with Geometry;         -- parent
with Geometry.Shapes;  -- child (parent automatically visible)
with Ada.Text_IO;

procedure Main is
   P : Geometry.Point  := (X => 0.0, Y => 0.0);
   C : Geometry.Shapes.Circle := (Center => P, Radius => 5.0);
begin
   Ada.Text_IO.Put_Line (Float'Image (Geometry.Shapes.Area (C)));
end Main;

-- Attributes are properties of types and objects, accessed with tick ('
-- Scalar type attributes
type Day is (Mon, Tue, Wed, Thu, Fri, Sat, Sun);

Lo  : Day     := Day'First;         -- Mon  (first value)
Hi  : Day     := Day'Last;          -- Sun  (last value)
Img : String  := Day'Image (Wed);   -- 'WED' (uppercase string)
V   : Day     := Day'Value ('FRI'); -- Fri  (string -> enum, raises Constraint_Error if bad)
Pos : Integer := Day'Pos (Mon);     -- 0    (zero-based position)
D   : Day     := Day'Val (4);       -- Fri  (position -> value)
Suc : Day     := Day'Succ (Mon);    -- Tue  (successor)
Pre : Day     := Day'Pred (Sun);    -- Sat  (predecessor)

-- Integer / range attributes
type Percent is range 0 .. 100;
Lo_P : Integer := Percent'First;   -- 0
Hi_P : Integer := Percent'Last;    -- 100
Wid  : Integer := Percent'Width;   -- character width of Image

-- Array attributes
type Arr is array (1 .. 10) of Integer;
A : Arr := (others => 0);
F   : Integer := A'First;           -- 1
L   : Integer := A'Last;            -- 10
Len : Integer := A'Length;          -- 10
-- A'Range  is the subtype 1 .. 10  (use in for loops)

-- Object attributes
X   : Integer := 42;
S   : Integer := Integer'Size;      -- 32 (bits on typical 32-bit platform)
Adr : System.Address := X'Address; -- memory address of X (needs with System)

-- Floating-point attributes
E   : Float   := Float'Epsilon;    -- smallest value where 1.0 + E /= 1.0
Dig : Integer := Float'Digits;     -- decimal digits of precision
Safe_Max : Float := Float'Safe_Last;

with Ada.Text_IO;       use Ada.Text_IO;
with Ada.Integer_Text_IO;
with Ada.Float_Text_IO;

procedure IO_Demo is
   N : Integer;
   F : Float;
   C : Character;
   S : String (1 .. 80);
   Last : Natural;
begin
   -- Put / Put_Line
   Put      ('Hello');            -- no newline
   Put_Line ('World');            -- with newline
   New_Line;                      -- blank line
   New_Line (3);                  -- three blank lines

   -- Integer I/O (instantiated package)
   Ada.Integer_Text_IO.Put (42, Width => 5);   -- '   42' (right-aligned in 5 chars)
   Ada.Integer_Text_IO.Get (N);                -- read integer from stdin

   -- Float I/O
   Ada.Float_Text_IO.Put (3.14159, Fore => 2, Aft => 4, Exp => 0);  -- '3.1416'
   Ada.Float_Text_IO.Get (F);

   -- Character I/O
   Put  (Character'('A'));
   Get  (C);

   -- String I/O
   Get_Line (S, Last);            -- reads up to newline; Last = last char index
   Put_Line (S (1 .. Last));      -- print only what was read

   -- File I/O
   declare
      File : File_Type;
   begin
      Create (File, Out_File, 'output.txt');   -- create/overwrite
      Put_Line (File, 'Written to file');
      Close (File);

      Open (File, In_File, 'output.txt');      -- read mode
      declare
         Line : String (1 .. 200);
         Len  : Natural;
      begin
         Get_Line (File, Line, Len);
         Put_Line (Line (1 .. Len));
      end;
      Close (File);
   end;
end IO_Demo;

with Ada.Numerics;                              -- Pi, e constants
with Ada.Numerics.Elementary_Functions;         -- Sqrt, Sin, Cos, Log, Exp...
with Ada.Numerics.Float_Random;                 -- random floats in [0, 1)
with Ada.Numerics.Discrete_Random;             -- random integers over a range

procedure Numerics_Demo is
   use Ada.Numerics.Elementary_Functions;

   X   : Float  := Ada.Numerics.Pi;            -- 3.14159265358979...
   E   : Float  := Ada.Numerics.E;             -- 2.71828...
   Y   : Float  := Sqrt (2.0);                 -- 1.41421...
   S   : Float  := Sin (Ada.Numerics.Pi / 2.0); -- 1.0
   L   : Float  := Log (Ada.Numerics.E);        -- 1.0
   P   : Float  := 10.0 ** 3.0;               -- 1000.0 (floating power)

   -- Fixed-point: exact decimal arithmetic
   type Money is delta 0.01 range -1_000_000.00 .. 1_000_000.00;
   Price : Money := 9.99;
   Tax   : Money := 0.80;
   Total : Money := Price + Tax;                -- 10.79 (no rounding error)

   -- Float random
   package RNG is new Ada.Numerics.Float_Random;
   Gen : RNG.Generator;
   R   : Float;

   -- Discrete random (over a user-defined range)
   type Die is range 1 .. 6;
   package Die_RNG is new Ada.Numerics.Discrete_Random (Die);
   Die_Gen : Die_RNG.Generator;
   Roll    : Die;

begin
   RNG.Reset (Gen);                             -- seed from clock
   R := RNG.Random (Gen);                      -- in [0.0, 1.0)

   Die_RNG.Reset (Die_Gen);
   Roll := Die_RNG.Random (Die_Gen);           -- 1 .. 6
end Numerics_Demo;

with Ada.Containers.Vectors;
with Ada.Containers.Hashed_Maps;
with Ada.Containers.Ordered_Maps;
with Ada.Containers.Hashed_Sets;
with Ada.Strings.Hash;

procedure Containers_Demo is

   -- Vector (dynamic array)
   package Int_Vec is new Ada.Containers.Vectors
      (Index_Type => Natural, Element_Type => Integer);
   use Int_Vec;

   V : Vector;
begin
   Append (V, 10);
   Append (V, 20);
   Append (V, 30);
   V.Prepend (5);                     -- 5 at front
   declare
      E : Integer := Element (V, 0);  -- 5 (zero-based index)
   begin
      null;
   end;
   for I in V.First_Index .. V.Last_Index loop
      null;   -- access V (I)
   end loop;
   for E of V loop                    -- for-of loop (Ada 2012)
      null;
   end loop;
   Delete (V, 1);                     -- remove element at index 1
   Ada.Text_IO.Put_Line (V.Length'Image);

   -- Hashed Map (String -> Integer)
   package Str_Int_Map is new Ada.Containers.Hashed_Maps
      (Key_Type        => Ada.Strings.Unbounded.Unbounded_String,
       Element_Type    => Integer,
       Hash            => Ada.Strings.Unbounded.Hash,
       Equivalent_Keys => Ada.Strings.Unbounded.'=');
   use Str_Int_Map;

   M : Str_Int_Map.Map;
   K : Ada.Strings.Unbounded.Unbounded_String :=
         Ada.Strings.Unbounded.To_Unbounded_String ('alice');
begin
   Insert (M, K, 95);
   M.Include (K, 100);                -- insert or update
   if M.Contains (K) then
      Ada.Text_IO.Put_Line (Integer'Image (M.Element (K)));
   end if;
   for C in M.Iterate loop
      null;   -- Str_Int_Map.Key (C), Str_Int_Map.Element (C)
   end loop;
end Containers_Demo;

with Ada.Text_IO;                  use Ada.Text_IO;
with Ada.Strings.Fixed;            use Ada.Strings.Fixed;
with Ada.Strings.Bounded;
with Ada.Strings.Unbounded;        use Ada.Strings.Unbounded;

procedure Strings_Demo is

   -- 1. Fixed-length String (standard Ada String)
   S : String (1 .. 20) := (others => ' ');
   -- Concatenation
   T : String := 'Hello' & ', ' & 'Ada!';  -- 'Hello, Ada!'
   -- Slice
   Sub : String := T (1 .. 5);              -- 'Hello'
   -- Comparison (lexicographic)
   B : Boolean := (T = 'Hello, Ada!');      -- True

   -- Ada.Strings.Fixed operations
   Found : Natural := Index (T, 'Ada');     -- 8 (1-based position)
   U     : String  := To_Upper (Sub);       -- 'HELLO'  (Ada.Strings.Maps.Constants)

   -- 2. Bounded_String: string with a compile-time maximum length
   package BS is new Ada.Strings.Bounded.Generic_Bounded_Length (Max => 100);
   use BS;

   BS1 : Bounded_String := To_Bounded_String ('Hello');
   BS2 : Bounded_String := BS1 & To_Bounded_String (' World');
   Len : Natural        := Length (BS2);    -- 11

   -- 3. Unbounded_String: dynamic, heap-allocated (most convenient)
   US1 : Unbounded_String := To_Unbounded_String ('Hello');
   US2 : Unbounded_String := US1 & ' World';   -- concatenate
   US1 := US1 & '!';                           -- append
   L   : Natural          := Length (US1);     -- 6
   Raw : String           := To_String (US1);  -- back to String

   -- Searching in Unbounded_String
   Pos : Natural := Index (US2, 'World');       -- 7

begin
   Put_Line (T);
   Put_Line (U);
   Put_Line (To_String (US2));
end Strings_Demo;

-- SPARK 2014 is a formally verifiable subset of Ada 2012.
-- Contracts are specified as aspects; GNATprove verifies them statically.

pragma SPARK_Mode (On);   -- enable SPARK analysis for this unit

package Account
   with SPARK_Mode
is
   type Balance_Type is range 0 .. 1_000_000;

   type Account_Type is private;

   function  Get_Balance (A : Account_Type) return Balance_Type;
   procedure Deposit     (A : in out Account_Type; Amount : Balance_Type)
      with Pre  => Amount > 0
                   and then Get_Balance (A) <= Balance_Type'Last - Amount,
           Post => Get_Balance (A) = Get_Balance (A)'Old + Amount;

   procedure Withdraw    (A : in out Account_Type; Amount : Balance_Type)
      with Pre  => Amount <= Get_Balance (A),
           Post => Get_Balance (A) = Get_Balance (A)'Old - Amount;

private
   type Account_Type is record
      Balance : Balance_Type := 0;
   end record;
end Account;

package body Account
   with SPARK_Mode
is
   function Get_Balance (A : Account_Type) return Balance_Type is (A.Balance);

   procedure Deposit (A : in out Account_Type; Amount : Balance_Type) is
   begin
      A.Balance := A.Balance + Amount;
   end Deposit;

   procedure Withdraw (A : in out Account_Type; Amount : Balance_Type) is
   begin
      A.Balance := A.Balance - Amount;
   end Withdraw;
end Account;

-- Loop invariant and assertion
procedure Sum_Array (A : array (Integer range <>) of Natural;
                     S : out Natural)
   with SPARK_Mode,
        Post => S = (for all I in A'Range => A (I)'Old)   -- simplified
is
begin
   S := 0;
   for I in A'Range loop
      pragma Loop_Invariant (S <= Natural'Last - A (I));
      S := S + A (I);
   end loop;
end Sum_Array;

-- Ravenscar is a restricted subset of Ada tasking for high-integrity
-- real-time systems. It guarantees schedulability analysis and bans
-- dynamic task creation, selective accept, and abort.

pragma Profile (Ravenscar);   -- enforce the profile compiler-wide

with Ada.Real_Time; use Ada.Real_Time;

package Periodic_Tasks is

   -- Task types only (no anonymous tasks in Ravenscar)
   task type Sensor_Task is
      pragma Priority (10);
   end Sensor_Task;

   task type Control_Task is
      pragma Priority (20);   -- higher priority preempts Sensor_Task
   end Control_Task;

end Periodic_Tasks;

package body Periodic_Tasks is

   -- Shared state through a protected object (only allowed concurrency mechanism)
   protected Sensor_Data is
      pragma Priority (20);
      procedure Write (V : Float);
      function  Read  return Float;
   private
      Value : Float := 0.0;
   end Sensor_Data;

   protected body Sensor_Data is
      procedure Write (V : Float) is begin Value := V; end Write;
      function  Read  return Float is (Value);
   end Sensor_Data;

   task body Sensor_Task is
      Period    : constant Time_Span := Milliseconds (10);   -- 10 ms period
      Next_Time : Time := Clock + Period;
   begin
      loop
         delay until Next_Time;   -- release point; only delay until allowed
         Sensor_Data.Write (42.0);
         Next_Time := Next_Time + Period;
      end loop;
   end Sensor_Task;

   task body Control_Task is
      Period    : constant Time_Span := Milliseconds (20);
      Next_Time : Time := Clock + Period;
      V         : Float;
   begin
      loop
         delay until Next_Time;
         V := Sensor_Data.Read;
         -- process V ...
         Next_Time := Next_Time + Period;
      end loop;
   end Control_Task;

end Periodic_Tasks;

-- ── Best Practice: Strong Typing ──────────────────────────────────────────

-- Use distinct named types to prevent unit/domain confusion.
-- The compiler catches type mismatches at compile time at zero runtime cost.

type Meters  is new Float;
type Seconds is new Float;
type Kg      is new Float;

Speed : Meters  := 100.0;
Time  : Seconds := 9.58;
Mass  : Kg      := 70.0;

-- Speed / Time would be Meters/Seconds -- but Ada won't let you mix types:
-- Bad : Float := Speed / Time;   -- ILLEGAL without explicit conversion
-- Correct: use a new derived type for the result
type Meters_Per_Second is new Float;
V : Meters_Per_Second := Meters_Per_Second (Speed) / Meters_Per_Second (Time);

-- Use range constraints to express invariants
type Port_Number    is range 0 .. 65535;
type HTTP_Status    is range 100 .. 599;
type Percentage     is range 0 .. 100;
type Temperature_K  is new Float range 0.0 .. Float'Last;  -- Kelvin >= 0

-- Use subtypes for aliases that share the parent's operations
subtype Even_Natural is Natural
   with Dynamic_Predicate => Even_Natural mod 2 = 0;  -- Ada 2012 predicate

-- Use modular types for bit-level operations (no sign, wraps correctly)
type Word16  is mod 2**16;
type Byte    is mod 256;
B : Byte := 2#1010_0101#;   -- binary literal
B := B and 2#0000_1111#;    -- 0x05

-- Enumeration types for named sets (not integer constants)
type Direction is (North, East, South, West);
type Suit      is (Clubs, Diamonds, Hearts, Spades);
-- avoid: North : constant Integer := 0; -- loses type safety

-- ── Best Practice: Contracts & SPARK ──────────────────────────────────────

-- Ada 2012 contracts: Pre/Post conditions, Type_Invariant, Subtype_Predicate
-- At runtime these raise Assertion_Error if violated (with -gnata).
-- With SPARK, GNATprove verifies them statically (no runtime cost needed).

-- Pre/Post on procedures
procedure Transfer (From, To : in out Account; Amount : Positive)
   with Pre  => From.Balance >= Amount
                and then To.Balance <= Integer'Last - Amount,
        Post => From.Balance = From.Balance'Old - Amount
                and then To.Balance = To.Balance'Old + Amount;

-- Type_Invariant: class-wide invariant enforced at package boundaries
package Stacks is
   type Stack is private
      with Type_Invariant => Stack.Size <= Stack.Capacity;

   function Push (S : Stack; X : Integer) return Stack
      with Pre => S.Size < S.Capacity;
end Stacks;

-- Subtype_Predicate for complex membership rules
subtype Prime is Positive
   with Dynamic_Predicate => Is_Prime (Prime);

-- Contract_Cases: exhaustive case analysis (SPARK)
function Clamp (X, Lo, Hi : Integer) return Integer
   with Pre            => Lo <= Hi,
        Contract_Cases =>
           (X < Lo     => Clamp'Result = Lo,
            X > Hi     => Clamp'Result = Hi,
            Lo <= X and X <= Hi => Clamp'Result = X);

-- Use pragma Assertion_Policy to enable/disable at build time:
--   pragma Assertion_Policy (Check);    -- enable (default in debug)
--   pragma Assertion_Policy (Ignore);   -- disable (release builds)

-- SPARK workflow:
--   1. annotate with Pre/Post/Invariant
--   2. run: gnatprove -P project.gpr
--   3. fix unproved VCs, add loop invariants / ghost code as needed

-- ── Best Practice: Tasking ─────────────────────────────────────────────────

-- Use protected objects for shared mutable state -- they are the safe,
-- efficient Ada monitor type. Never use plain shared variables.

protected type Counter is
   procedure Increment;
   procedure Decrement;
   function  Value return Integer;
   entry     Wait_For_Zero;           -- entry: blocked until guard is true
private
   N : Integer := 0;
end Counter;

protected body Counter is
   procedure Increment is begin N := N + 1; end Increment;
   procedure Decrement is begin N := N - 1; end Decrement;
   function  Value return Integer is (N);
   entry Wait_For_Zero when N = 0 is  -- guard: callers queue until N = 0
   begin null; end Wait_For_Zero;
end Counter;

-- Use task types (not anonymous tasks) for reusability and testability.
task type Worker (Priority : Integer := 10) is
   pragma Priority (Priority);
   entry Start;
   entry Stop;
end Worker;

-- Use selective accept for non-blocking rendezvous alternatives
task body Server is
begin
   loop
      select
         accept Request (X : in Integer; Y : out Integer) do
            Y := X * 2;
         end Request;
      or
         accept Shutdown;
         exit;              -- clean exit
      or
         delay 5.0;         -- timeout: run maintenance after 5 s idle
         Flush_Buffers;
      end select;
   end loop;
end Server;

-- Never use shared unprotected variables between tasks.
-- Prefer rendezvous or protected objects over busy-waiting.
-- For real-time: use Ravenscar profile for deterministic scheduling.

-- ── Best Practice: Exception Handling ─────────────────────────────────────

-- Declare exceptions at the right scope level -- package level for library,
-- local for internal logic.
package Database is
   Connection_Failed : exception;
   Query_Error       : exception;
end Database;

-- Provide informative messages using raise ... with 'message'
procedure Connect (Host : String; Port : Natural) is
begin
   if Port = 0 then
      raise Database.Connection_Failed
         with 'Invalid port 0 for host ' & Host;
   end if;
end Connect;

-- Handle exceptions as specifically as possible; avoid 'when others' swallowing
procedure Run is
begin
   Connect ('localhost', 0);
exception
   when Database.Connection_Failed =>
      Ada.Text_IO.Put_Line ('Cannot connect -- check host/port');
   when Database.Query_Error =>
      Ada.Text_IO.Put_Line ('Query failed -- retrying...');
   when E : others =>
      -- Log and re-raise; do not silently discard unknown exceptions
      Ada.Text_IO.Put_Line
         ('Unhandled: ' & Ada.Exceptions.Exception_Information (E));
      raise;
end Run;

-- Use exception occurrence for structured logging
with Ada.Exceptions;
procedure Log_Exception (E : Ada.Exceptions.Exception_Occurrence) is
begin
   Ada.Text_IO.Put_Line ('Exception: ' & Ada.Exceptions.Exception_Name (E));
   Ada.Text_IO.Put_Line ('Message  : ' & Ada.Exceptions.Exception_Message (E));
   -- Ada.Exceptions.Save_Occurrence stores it for later inspection
end Log_Exception;

-- Do not use exceptions for normal control flow (Constraint_Error for loop end etc.)
-- Use attributes like 'First/'Last and explicit range checks instead.
-- Assert invariants with pragma Assert or Pre/Post rather than catching exceptions.

-- ── Best Practice: Packages & Abstraction ─────────────────────────────────

-- Keep the spec (ads) minimal: expose only what clients need.
-- Put implementation details in the private section or the body (adb).

package Queue
   with Pure   -- package has no mutable state visible to clients
is
   -- Opaque private type: clients cannot see or construct internals
   type Queue_Type is private;

   -- Constructor: only legal way to create a Queue_Type
   function  Empty    return Queue_Type;
   procedure Enqueue  (Q : in out Queue_Type; X : Integer);
   procedure Dequeue  (Q : in out Queue_Type; X : out Integer)
      with Pre => not Is_Empty (Q);
   function  Is_Empty (Q : Queue_Type) return Boolean;
   function  Length   (Q : Queue_Type) return Natural;

private
   -- Exposed to the body and child packages, hidden from all others
   Max : constant := 1000;
   type Data_Array is array (1 .. Max) of Integer;
   type Queue_Type is record
      Data  : Data_Array;
      Head  : Natural := 0;
      Tail  : Natural := 0;
      Count : Natural := 0;
   end record;
end Queue;

-- Child packages for extending without recompiling the parent
package Queue.IO is
   procedure Print (Q : Queue_Type);  -- accesses parent private section
end Queue.IO;

-- Use 'with' clauses selectively: only depend on what you actually use.
-- Prefer 'use type' (Ada 2005) over blanket 'use' to avoid name clashes:
with Ada.Containers.Vectors;
use type Ada.Containers.Count_Type;   -- makes = /= etc. available, not all names

-- Avoid circular dependency: factor common types into a third package.

-- ── Best Practice: Portability & Safety ───────────────────────────────────

-- Use implementation-defined sizes via System package when needed
with System;
Bits_Per_Integer : constant := Integer'Size;   -- e.g., 32 or 64
Word_Size        : constant := System.Word_Size;

-- For fixed-size types, use Interfaces package
with Interfaces;
X8  : Interfaces.Unsigned_8  := 16#FF#;
X16 : Interfaces.Unsigned_16 := 16#FFFF#;
X32 : Interfaces.Integer_32  := -1;

-- Specify record layout for hardware/protocol compatibility
type Packet is record
   Version  : Interfaces.Unsigned_8;
   Flags    : Interfaces.Unsigned_8;
   Length   : Interfaces.Unsigned_16;
end record;
for Packet use record
   Version at 0 range 0 .. 7;
   Flags   at 1 range 0 .. 7;
   Length  at 2 range 0 .. 15;
end record;
for Packet'Size use 32;   -- enforce exact wire size

-- Avoid implementation-defined behavior:
-- Use 'Size, 'First, 'Last attributes instead of assuming ranges.
-- Use Shift_Left / Shift_Right from Interfaces, not unchecked conversions.
with Interfaces; use Interfaces;
B : Unsigned_16 := Shift_Left (1, 8);   -- 256: portable bit shift

-- Use pragma Suppress carefully and only with proof that checks are redundant
-- pragma Suppress (Range_Check);   -- only in proven SPARK code

-- Prefer standard library packages over system-specific ones:
--   Ada.Text_IO, Ada.Directories, Ada.Calendar, Ada.Real_Time
-- Mark non-portable code with pragma Warnings (Off, ...) and a comment.

-- Enable full compiler checks in development:
--   -gnata   enable assertions and pre/post
--   -gnatwa  all warnings
--   -gnatwe  warnings as errors
--   -gnaty   style checks