package queue;

//n - count of elements in queue
//a[i] - element on position "i"

public class ArrayQueueADT {
    // Inv: (n >= 0) && (a[i] != null for i = 1..n - 1)
    private Object[] elements = new Object[10];
    private int size = 0;
    private int head = 0;
    private int tail = 0;

    // Pre: capacity >= 0
    private static void ensureCapacity(ArrayQueueADT queue, int capacity) {
        if (capacity <= queue.elements.length) {
            return;
        }

        int newlength = 2 * capacity;
        Object[] newQueue = new Object[newlength];
        for (int i = queue.size - 1; i >= queue.head; i--) {
            newlength--;
            newQueue[newlength] = queue.elements[i];
        }
        queue.head = newlength;
        for (int i = 0; i < queue.tail; i++) {
            newQueue[i] = queue.elements[i];
        }
        queue.elements = newQueue;
    }
    // Post: (n' == n) && (a'[i] == a[i] for i = 0...n - 1)

    // Pre: element != null
    public static void enqueue(ArrayQueueADT queue, Object element) {
        assert element != null;

        ensureCapacity(queue, queue.size + 1);
        queue.size++;
        queue.elements[queue.tail] = element;
        queue.tail = (queue.tail + 1) % queue.elements.length;
    }
    // Post: (n' == n + 1) && (a'[i] == a[i] for i = 0..n - 1) && (a'[n] == element)

    // Pre: n > 0
    public static Object dequeue(ArrayQueueADT queue) {
        assert size(queue) > 0;

        Object x = queue.elements[queue.head];
        queue.elements[queue.head] = null;
        queue.head = (queue.head + 1) % queue.elements.length;
        queue.size--;
        return x;
    }
    // Post: (n' == n - 1) && (a'[i - 1] == a[i] for i = 1...n - 1) && (Result == a[0])

    // Pre: n > 0
    public static Object element(ArrayQueueADT queue) {
        assert queue.size > 0;

        return queue.elements[queue.head];
    }
    // Post: (n' == n) && (a'[i] == a[i] for i = 0...n - 1) && (Result == a[0])

    // Pre: element != null
    public static void push(ArrayQueueADT queue, Object element) {
        assert element != null;

        ensureCapacity(queue, queue.size + 1);
        queue.size++;
        queue.head = (queue.head - 1 + queue.elements.length) % queue.elements.length;
        queue.elements[queue.head] = element;
    }
    // (n' == n + 1) && (a'[i + 1] == a[i] for i = 0..n - 1) && (a'[0] == element)

    // Pre: n > 0
    public static Object peek(ArrayQueueADT queue) {
        assert queue.size > 0;

        return queue.elements[(queue.tail - 1 + queue.elements.length) % queue.elements.length];
    }
    // Post: (n' == n) && (a'[i] == a[i] for i = 0...n - 1) && (Result == a[n - 1])

    // Pre: n > 0
    public static Object remove(ArrayQueueADT queue) {
        assert queue.size > 0;

        Object result = queue.elements[(queue.tail - 1 + queue.elements.length) % queue.elements.length];
        queue.elements[(queue.tail - 1 + queue.elements.length) % queue.elements.length] = null;
        queue.tail = (queue.tail - 1 + queue.elements.length) % queue.elements.length;
        queue.size--;
        return result;
    }
    // Post: (n' == n - 1) && (a'[i] == a[i] for i = 0...n - 2) && (Result == a[n - 1])

    public static int size(ArrayQueueADT queue) {
        return queue.size;
    }
    // Post: (n' == n) && (a'[i] == a[i] for i = 0...n - 1) && (Result == n)

    public static boolean isEmpty(ArrayQueueADT queue) {
        return queue.size == 0;
    }
    // Post: (n' == n) && (a'[i] == a[i] for i = 0...n - 1) && (Result == (n == 0))

    public static void clear(ArrayQueueADT queue) {
        queue.size = queue.head = queue.tail = 0;
    }
    // Post: n == 0
}