types
	Queue, Integer, Boolean

var
	q, x:xq : Queue;
	i 	: Integer;

operations
	empty 	: --> Queue
	add 	: Queue x Integer --> Queue
	front 	: Queue --> Integer
	remove 	: Queue --> Queue
	isEmpty : Queue --> Boolean
	
preconditions
	pre-remove(q)       = not isEmpty(q)
	pre-front(q) 	    = not isEmpty(q)	

axioms
	isEmpty(empty())    = true
	isEmpty(add(q,i))   = false
	remove(add(x:xq,i)) = xq:i
	front(add(x:xq,i))  = x