package Queue_Pack_Contract is

type Element is new Positive range 1 .. 1000;

type Queue_Type is private;

type Marker is mod Queue_Size;

type List is array (Marker) of Element;

Queue_Size : constant Positive := 10;

procedure Enqueue 
(
Item
:     Element;
Q
: in out Queue_Type) with Pre  => not Is_Full (Q), Post => not Is_Empty (Q) and then Length (Q) = Length (Q'Old) + 1 and then Lookahead (Q, Length (Q)) = Item and then (for all ix in 1 .. Length (Q'Old) => Lookahead (Q, ix) = Lookahead (Q'Old, ix));

procedure Dequeue 
(
Item
: out Element;
Q
: in out Queue_Type) with Pre  => not Is_Empty (Q), Post => not Is_Full (Q) and then Length (Q) = Length (Q'Old) - 1 and then (for all ix in 1 .. Length (Q) => Lookahead (Q, ix) = Lookahead (Q'Old, ix + 1));

function Is_Empty  
(
Q
: Queue_Type) return Boolean;

function Is_Full   
(
Q
: Queue_Type) return Boolean;

function Length    
(
Q
: Queue_Type) return Natural;

function Lookahead 
(
Q
: Queue_Type;
Depth
: Positive) return Element;