Nosaltres: Especificación formal e implementación de tipos abstractos de datos básicos