class UnboundedStack { UnboundedStack() : {} { Stack(this, nil()) }; void push(Object val) : { Stack(this, vs) } { Stack(this, cons(val,vs)) }; Object pop() : { Stack(this, cons(v,vs)) } { Stack(this, vs) * v == return}; boolean isEmpty() : { Stack(this, vs) } { Stack(this, vs) * (return==false() * vs == cons(_,_) || return==true() * vs == nil() ) }; }