Text this: Técnicas de especificación formal de sistemas orientados a objetos basadas en lógica de reescritura