refinement<E>
    Element is E

    Queue[Element] is SLLQueue<E> {
        make: --> Queue[Element]
        is
        SLLQueue();
        
        enqueue: Queue[Element] e:Element --> Queue[Element]
        is
        void enqueue(E e);

        front: Queue[Element] -->? Element
        is
        E front();
        
        dequeue: Queue[Element] -->?Queue[Element]
        is
        void dequeue();
        
        isEmpty: Queue[Element]
        is
        boolean isEmpty();
        
        size: Queue[Element] --> int
        is
        int size();
    }
end refinement