refinement<E>
  
  Element is E

  Stack[Element] is ArrayStack<E> {
    
    make: --> Stack[Element] 	
    				is ArrayStack();
    
    push: Stack[Element] e:Element --> Stack[Element] 
    				is void push(E e);
    
    pop: Stack[Element] -->? Stack[Element] 
   					is void pop();
    
    peek: Stack[Element] -->? Element 
    				is E peek();
    
    isEmpty: Stack[Element] 
    				is boolean isEmpty();
   }

end refinement