Maude 2.6
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.