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