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

\pre{\lng{r} \leq \floor{MAX/2}}
\cpre{\lng{r} \leq MAX - \lng{self}}
\nomop{Put(r)}
\post{self\sal = self\ent + r}
\vspace{-2ex}\\

\pre{n \leq \floor{MAX/2}}
\cpre{\lng{self} \geq n}
\nomop{Get(n, s)}
\post{self\ent = self\sal + s}
\vspace{-2ex}
%
\end{ctadsol}
