Term rewriting is a widely used technique for executing equationai logic programs. This paper describes the design methodology used in the rigorous development of a rewrite rule interpreter for UMIST OBJ, a language for expressing executable algebraic specifications of programs. The design methodology was inspiredby the use of UMIST OBJ itself as a development tool.