My first experience with SPARK-Ada

with Ada.Strings.Unbounded;     use Ada.Strings.Unbounded;

package Token_Lists 
   with SPARK_Mode => On -- This specs is in SPARK
is

   subtype List_Length is Integer range 1 .. Integer'Last;

   -- "Tagged types" correspond roughly to what other 
   -- languages call "class".  Token_List is the desired
   -- pseudo-vector for holding the pieces.  
   --
   -- The funny (<>) means that the type is parameterized, but the
   -- parameter is not public.  This forces you to initialize 
   -- any variable of type Token_List with some kind of constructor.
   --
   -- Finally, "private" means that the internal details are not
   -- visible and are described later, in the private part. 
   --
   type Token_List (<>) is tagged private;

   function Create (N : List_Length) return Token_List
     with
       Post =>
         Create'Result.Capacity = N and Create'Result.Length = 0;
    --
    -- Post is an "attribute" and it specifies a Boolean expression
    -- that will be true when the function returns (contract). 
    --
    -- The post-condition says that the created list will have 
    -- room for N entries and it will be empty
    --

   function Capacity (Item : Token_List) return Positive;

   function Length (Item : Token_List) return Natural
     with Post => Length'Result <= Item.Capacity;
   --
   -- Number of the pieces currently in the list.  Of course 
   -- it cannot be larger than the capacity, if it happens 
   -- there is something wrong somewhere...
   ---

   procedure Append (List : in out Token_List;
                     What : String)
     with
       Pre'Class =>
         List.Length  < List.Capacity,

       Post =>
         List.Length = List.Length'Old + 1
     and List.Capacity = List.Capacity'Old;
    -- 
    -- The precondition (attribute "Pre") says that before calling
    -- the procedure there must be some room in the list; the
    -- post condition says that after the call there is a new entry,
    -- but the capacity is unchanged (it is obvious to you, not to
    -- SPARK).  SPARK will analyze the body of Append and it 
    -- will try to prove that the contract is respected, that is, 
    -- that the postcondition follows from the precondition.
    --
    -- If you arm correctly the code that calls Append, SPARK will
    -- try to prove that the precondition is always verified. If it  
    -- succeeds you know you'll never have an overflow!
    --

private
   --
   -- Some privacy needed... :-)
   --


   type Token_Array is array (Positive range <>) of Unbounded_String;
   --
   -- The funny "(Positive range <>)" says that the index of 
   -- indexes of a variable of type Token_Array is a range of
   -- positive integers.  
   -- 
   -- Yes, in Ada the array indexes do not *necessarily* start
   -- from zero... They can start from whatever you want... ;-D
   --

   type Token_List (Length : List_Length) is tagged
      record
         Tokens     : Token_Array (1 .. Length) := (others => Null_Unbounded_String);
         First_Free : Positive := 1;
      end record
     with 
       Predicate => 
         Token_List.First_Free <= Integer (Token_List.Length) + 1
     and Token_List.Tokens'Length = Token_List.Length;
    -- 
    -- This is the full definition of Token_List anticipated 
    -- in the public part above.  In Ada it is not possible 
    -- to have some field public and some private (like in C++
    -- or Ruby).  If you put the full definition in the public
    -- part, everything is public (typically considered bad practice),
    -- otherwise everything is private.  Honestly, I never felt the
    -- need of the hybrid solution.
    -- 
    -- "Predicate" is another attribute.  It specifies a condition
    -- that a variable of type Token_List must always satisfy.
    --
    -- If you ask to the compiler to check assertions, the 
    -- compiler will produce code that checks the predicate
    -- at the end of methods ("primitive procedures" in Ada 
    -- jargon) that modify the variable and if the condition 
    -- is not satisfied, an exception is raised, pointing an
    -- accusing finger against the culprit.  
    --
    -- A powerful bug trap!
    --



   function Create (N : List_Length) return Token_List
   is (Token_List'(Length     => N,
                   Tokens     => (others => Null_Unbounded_String),
                   First_Free => 1));

   function Capacity (Item : Token_List) return Positive
   is (Item.Tokens'Last);

   function Length (Item : Token_List) return Natural
   is (Item.First_Free - 1);
end Token_Lists;

pragma Ada_2012;
package body Token_Lists 
   with SPARK_Mode => On -- This body is in SPARK
is

   ------------
   -- Append --
   ------------

   procedure Append
     (List : in out Token_List;
      What : String)
   is
   begin
      --
      -- If you look at the definition of Token_List 
      -- you'll see that List.Tokens is an array. 
      -- List.Tokens'Last is the last index of Lists.Tokens
      -- 
      if List.First_Free > List.Tokens'Last then
         raise Constraint_Error;
      end if;

      List.Tokens (List.First_Free) := To_Unbounded_String (What);
      List.First_Free := List.First_Free + 1;
   end Append;

end Token_Lists;

 [Counterexample] List = (Length => ?, First_Free => 2147483647) 
 and List.Tokens'First = 1 and List.Tokens'Last = 2147483647

subtype List_Length is Integer range 1 .. Integer'Last;

subtype List_Length is Integer range 1 .. Integer'Last-1;

function Create (N : List_Length) return Token_List;