Maude is a high-performance reflective specification and
programming language for a wide range of applications.
Besides supporting order sorted equational algebra (in the
style of OBJ3), it also supports a more general rewriting
logic which need not be confluent or terminating. In this way,
it is particularly suited for modeling concurrent object-
oriented computation. It also includes various environments
such as a model checker and an interactive theorem prover.
