Fully verifying transformation contracts for declarative ATL | Publicación