Abstract. Object-oriented language concepts have been highly successful, resulting in a large number of object-oriented languages and language extensions. Unfortunately, formal methods for defining and reasoning about these languages are still often performed after the fact, potentially resulting in ambiguous, overly complex, or poorly understood language features. We believe it is important to bring the use of formal techniques forward in this process, using them as an aid to language design and evolution. To this end, we propose a set of tools and techniques, making use of rewriting logic, to provide an interactive environment for the design and evolution of object-oriented languages, while also providing a solid mathematical foundation for language analysis and verification. Key words: object-oriented languages, programming language semantics, language design, rewriting logic, formal analysis 1 Problem Description Object-oriented languages and design techniques have been highly su...