package framework.util;

/**
 * Utility class representing a ring buffer.
 */
public class RingBuffer {
    /**
     * Create an empty RingBuffer object of the specified capacity.
     * @param  c the capacity
     */
    public RingBuffer(int c) {
        capacity    = c;
        size        = 0;
        first       = 0;
        last        = 0;
        buffer      = new Double[capacity];
    }

    /**
     * Get the current number of items stored in the buffer.
     * @return the number of items
     */
    public int size() {
        return size;
    }

    /**
     * Test if the buffer is empty.
     * @return true if is empty, false otherwise
     */
    public boolean isEmpty() {
        return size == 0;
    }

    /**
     * Test if the buffer is full.
     * @return true if it is full, false otherwise
     */
    public boolean isFull() {
        return size == capacity;
    }

    /**
     * Add item at the end of the list.
     * @param x the item to be added
     */
    public void enqueue(Double x) {
        buffer[last]    = x;
        last            = (last + 1) % capacity;
        size++;
    }

    /**
     * Delete and return the item at the front of the list.
     * @return the deleted item
     */
    public Double dequeue() {
        Double item = buffer[first];
        first       = (first + 1) % capacity;
        size--;
        return item;
    }

    /**
     * Return but do not delete the item at the front of the list.
     * @return the item at the front
     */
    public Double peek() {
        return buffer[first];
    }

    Double[]    buffer;
    int         capacity;
    int         first;
    int         last;
    int         size;
}
@@ -203,16 +203,75 @@
 apacity%0A
+     * @postcondition size == 0 && first == 0 && last == 0%0A
      */%0A
@@ -445,16 +445,145 @@
 acity%5D;%0A
+        assert size == 0 && first == 0 && last == 0:%0A            %22violated postcondition: size == 0 && first == 0 && last == 0%22;%0A
     %7D%0A%0A 
@@ -1177,382 +1177,1262 @@
    *
-/%0A    public void enqueue(Double x) %7B%0A        buffer%5Blast%5D    = x;%0A        last            = (last + 1) %25 capacity;%0A        size++;%0A    %7D%0A%0A    /**%0A     * Delete and return the item at the front of the list.%0A     * @return the deleted item%0A     */%0A    public Double dequeue() %7B%0A        Double item = buffer%5Bfirst%5D;%0A        first       = (first + 1) %25 capacity;%0A        size--
+ @precondition    size %3C capacity%0A     * @postcondition   size %3E 0 && size %3C= capacity%0A     * @postcondition   last %3E= 0 && last %3C= capacity%0A     */%0A    public void enqueue(Double x) %7B%0A        assert size %3C capacity: %22violated precondition: size %3C capacity%22;%0A%0A        buffer%5Blast%5D    = x;%0A        last            = (last + 1) %25 capacity;%0A        size++;%0A%0A        assert size %3E 0 && size %3C= capacity:%0A            %22violated postcondition: size %3E 0 && size %3C= capacity%22;%0A        assert last %3E= 0 && last %3C= capacity:%0A            %22violated postcondition: last %3E= 0 && last %3C= capacity%22;%0A    %7D%0A%0A    /**%0A     * Delete and return the item at the front of the list.%0A     * @return the deleted item%0A     * @precondition size %3E 0%0A     * @postcondition size %3E= 0 && size %3C capacity%0A     * @postcondition first %3E= 0 && first %3C= capacity%0A     */%0A    public Double dequeue() %7B%0A        assert size %3E 0: %22violated precondition: size %3E 0%22;%0A%0A        Double item = buffer%5Bfirst%5D;%0A        first       = (first + 1) %25 capacity;%0A        size--;%0A%0A        assert size %3E= 0 && size %3C capacity:%0A            %22violated postcondition: size %3E= 0 && size %3C capacity%22;%0A        assert first %3E= 0 && first %3C= capacity:%0A            %22violated postcondition: first %3E= 0 && first %3C= capacity%22
 ;%0A  

Add pre and post conditions to RingBuffer.