\begin{ctadsol}
%
  \nombrectad{Boundedbuffer}
%
  \operaciones
  \operacion{Put}{\mathbb{N}[i]}
  \operacion{Get}{\mathbb{N}[o]}
%
\semdom
\tipo{Boundedbuffer =  Sequence(ANY) }
  \invariante{\forall mb \in Boundedbuffer \st\ \lng{mb} \leq MAX}
  \inicial{self}{\lng{self} = 0}

  \pre{\true}
  \cpre{ \lng{self} \leq MAX - 1}
  \nomop{Put(r)}
  \post{self\sal = self\ent + r}

  \pre{\true}
  \cpre{1 \leq \lng{self}}
  \nomop{Get(s)}
  \post{self\ent = self\sal + s}
%
\end{ctadsol}
