Principles of Maude

This paper introduces the basic concepts of the rewriting logic language Maude and discusses its implementation. Maude is a wide-spectrum language supporting formal specification, rapid prototyping, and parallel programming. Maude's rewriting logic paradigm includes the functional and object-oriented paradigms as sublanguages. The fact that rewriting logic is reflective leads to novel metaprogramming capabilities that can greatly increase software reusability and adaptability. Control of the rewriting computation is achieved through internal strategy languages defined inside the logic. Maude's rewrite engine is designed with the explicit goal of being highly extensible and of supporting rapid prototyping and formal methods applications, but its semi-compilation techniques allow it to meet those goals with good performance.