1. -- 
  2. -- Uwe R. Zimmer, Australia, 2013 
  3. -- 
  4.  
  5. pragma Initialize_Scalars; 
  6.  
  7. package Queue_Pack_Contract is 
  8.  
  9.    Queue_Size : constant Positive := 10; 
  10.    type Element is new Positive range 1 .. 1000; 
  11.  
  12.    type Queue_Type is private; 
  13.  
  14.    procedure Enqueue (Item :     Element; Q : in out Queue_Type) with 
  15.      Pre  => not Is_Full (Q), 
  16.      Post => not Is_Empty (Q) and then Length (Q) = Length (Q'Old) + 1 
  17.                 and then Lookahead (Q, Length (Q)) = Item 
  18.                 and then (for all ix in 1 .. Length (Q'Old) => Lookahead (Q, ix) = Lookahead (Q'Old, ix)); 
  19.  
  20.    procedure Dequeue (Item : out Element; Q : in out Queue_Type) with 
  21.      Pre  => not Is_Empty (Q), 
  22.      Post => not Is_Full (Q) and then Length (Q) = Length (Q'Old) - 1 
  23.                 and then (for all ix in 1 .. Length (Q) => Lookahead (Q, ix) = Lookahead (Q'Old, ix + 1)); 
  24.  
  25.    function Is_Empty  (Q : Queue_Type) return Boolean; 
  26.    function Is_Full   (Q : Queue_Type) return Boolean; 
  27.    function Length    (Q : Queue_Type) return Natural; 
  28.    function Lookahead (Q : Queue_Type; Depth : Positive) return Element; 
  29.  
  30. private 
  31.    type Marker is mod Queue_Size; 
  32.    type List is array (Marker) of Element; 
  33.    type Queue_Type is record 
  34.       Top, Free : Marker  := Marker'First; 
  35.       Is_Empty  : Boolean := True; 
  36.       Elements  : List; -- will be initialized to invalids 
  37.    end record with Type_Invariant => (not Queue_Type.Is_Empty or else Queue_Type.Top = Queue_Type.Free) 
  38.      and then (for all ix in 1 .. Length (Queue_Type) => Lookahead (Queue_Type, ix)'Valid); 
  39.  
  40.    function Is_Empty (Q : Queue_Type) return Boolean is 
  41.      (Q.Is_Empty); 
  42.  
  43.    function Is_Full (Q : Queue_Type) return Boolean is 
  44.      (not Q.Is_Empty and then Q.Top = Q.Free); 
  45.  
  46.    function Length (Q : Queue_Type) return Natural is 
  47.      (if Is_Full (Q) then Queue_Size else Natural (Q.Free - Q.Top)); 
  48.  
  49.    function Lookahead (Q : Queue_Type; Depth : Positive) return Element is 
  50.      (Q.Elements (Q.Top + Marker (Depth - 1))); 
  51.  
  52. end Queue_Pack_Contract;