Maude system

The Maude system is an implementation of rewriting logic developed at SRI International. It is similar in its general approach to Joseph Goguen's OBJ3 implementation of equational logic, but based on rewriting logic rather than order-sorted equational logic, and with a heavy emphasis on powerful metaprogramming based on reflection.

Maude is free software, and tutorials are available online.

Maude modules (rewrite theories) consists of a term-language plus sets of equations and rewrite-rules. Terms in a rewrite theory are constructed using operators (functions taking 0 or more arguments of some sort, which return a term of a specific sort). Operators taking 0 arguments are considered constants, and one constructs their term-language by these simple constructs.

This rewrite theory specifies all the natural numbers. The sort saying is introduced, that there exists a sort called Nat (short for natural numbers), and below is the specification of how these terms are constructed. The operator s in Example 1 is the successor function representing the next natural number in the sequence of natural numbers i.e. s(N) := N + 1. s(0) is meant to represent the natural number 1 and so on. 0 is a constant, it takes no input parameter(s) but returns a Nat.

In Example 2 the + sign is introduced, meant to represent addition of natural numbers. Its definition is almost identical to the previous one, with input and output sorts but there is a difference, its operator has underscores on each side. Maude lets the user specify whether or not operators are infix, postfix or prefix (default), this is done using underscores as place fillers for the input terms. So the + operator takes its input on each side making it an infix operator. Unlike our previous operator s which takes its input terms after the operator (prefix).

The three stars are Maude's rest-of-line-comments and lets the parser know that it can ignore the rest of the line (not part of the program), with parenthesis meaning section comments:

The extended Nat module also holds two variables and two sets of equations.

When Maude "executes", it rewrites terms according to our specifications. And this is done with the statement

or the shorter form

...
Wikipedia