Invariant-driven specifications in Maude | Publicación