Bounded Stack

Let's start with a bounded stack example.

Bounded_Stack : generic
   type Element is hidden and <-;
Bounded_Stack : module is
   type Stack (Max_Size : General_Index_Value) is module
      Push : procedure (Item : in Element) when not Is_Full;
      -- Adds Item to the top of the stack.

      Pop : function return Element when not Is_Empty;
      -- Removes the top Element from the stack and returns it.

      Length : function return General_Count_Value;
      -- Returns the number of Elements on the stack.

      Is_Empty : function return Boolean;
      -- Returns Length = 0;

      Is_Full : function return Boolean;
      -- Returns Length = Max_Size;
   Stack : end;
Bounded_Stack : end;

The generic formal "type Element is hidden and <-;" specifies that the module will not use any operations of Element except assignment ("<-" in NINA) and any explicitly imported operations (none in this case). The actual must not be a no-assignment type. The similar generic formal "type Identifier is hidden;" specifies that the module will only use explicitly imported operations of the type; the actual may be a no-assignment type.

The "when Boolean_expression" part of the subprogram specifications is a precondition; these will be tested when the subprogram is called, and Constraint_Violation will be raised if the condition is False. 

Stack is a "module type." An object of a module type may be used exactly like a module. Module types are no-assignment types; assignment is not defined for them.

General_Count_Value and General_Index_Value are predefined subtypes similar to Ada's Natural and Positive from NINA_Predefined_Environment, NINA's equivalent of Ada's package Standard:

type General_Count_Value is range 0 .. 2 ** 64 - 1;

subtype General_Index_Value is General_Count_Value range 1 .. General_Count_Value'Last;