refinement<E>
    Element is E

    Dequeue[Element] is SLLDequeue<E> {
        make: --> Dequeue[Element]
        is
        SLLDequeue();
        
        addFirst: Dequeue[Element] e:Element --> Dequeue[Element]
        is
        void addFirst(E e);

        getFirst: Dequeue[Element] -->? Element
        is
        E getFirst();
        
        removeFirst: Dequeue[Element] -->?Dequeue[Element]
        is
        void removeFirst();
        
        isEmpty: Dequeue[Element]
        is
        boolean isEmpty();

        getLast: Dequeue[Element] -->? Element is E getLast();
        
        removeLast: Dequeue[Element] -->? Dequeue[Element]
        is
        void removeLast();
        
        addLast: Dequeue[Element] e:Element --> Dequeue[Element]
        is
        void addLast(E e);
        
        size: Dequeue[Element] --> int
        is
        int size();
    }
end refinement