Figure 2.1: Maude home page at maude.cs.uiuc.edu
The Maude system is available, free of charge, under the terms of the GNU General Public License as published by the Free Software Foundation, at the Maude home page (a snapshot is shown in Figure 2.1)
There you can also find documentation about Maude, including a Maude primer, some papers on Maude and rewriting logic, and several Maude applications, including a set of proving tools for Maude specifications and Maude case studies.
Maude binaries are provided for selected architectures and operating systems, including Linux and MacOS X. Detailed information on this can be found in the Maude web site, where installation instructions are also available.
A Maude session can be started by calling the maude.linux binary in the maude-linux/bin directory in a Linux shell window (and similarly for other platforms). For example, we can move into that directory and then invoke Maude, obtaining a banner similar to the following, where we can see the version of the system being executed, the date it was built, copyright information, and the current date.
The Maude system is now ready to accept Maude modules and commands (see Chapter 18 for a complete list of Maude commands). During a Maude session, the user interacts with the system by entering a request at the Maude prompt. For example, one can quit:
q may be used as an abbreviation of the quit command. But please, do not leave us so soon! One can also enter modules and use other commands. For example, we can enter the following module SIMPLE-NAT, which specifies the natural numbers in Peano notation with a plus operation _+_ on them.1
Fortunately, we do not need to write our modules in the prompt. We can input one or several modules by saving them in a file and then entering the file with the in or load commands (the only difference between both commands is that the latter does not produce detailed output as modules are entered). Assuming that the file my-nat.maude contains the module SIMPLE-NAT above, we can do the following to enter it:
After entering the module SIMPLE-NAT into Maude, we can, for example, reduce the term s s zero + s s s zero (which is the equivalent in Peano notation of the more usual 2 + 3) as follows:
It is not necessary to give the name of the module in which to reduce a term explicitly. All commands that require a module refer to the current module by default, unless a module is explicitly given. The current module is usually the last module entered or used, although we can use the select command to select a module to be the current one (see Section 18.13).
Any action happening in the Maude system can be interrupted by typing control-C. In particular, by hitting control-C during a reduction in progress, such reduction is interrupted and the system gets into debugging mode (see Section 14.1.3).
Although it is not the case in the simple examples above, sometimes we get a very big term as output from Maude. In some cases, in order to make it easier to read and understand, we edit the presentation of the outputs given by Maude.
When you execute maude.linux, the file prelude.maude, which includes several predefined modules (see Chapter 7), is automatically loaded. To find prelude.maude, the Maude interpreter checks for it in several directories, in the following order:
It is a good idea to include the path to prelude.maude in the MAUDE_LIB environment variable to be sure that it will always be found, because the executable finding code may not find the directory containing the executable.
Among the predefined modules included in prelude.maude we find a module STRING that declares sorts and operations for manipulating strings. In particular, STRING introduces the operation _+_ to concatenate two strings. Then, to concatenate the strings “hello”, “ ”, and “world”, you can type at the Maude prompt the following red (which is the abbreviated form of reduce) request:
Actually, although STRING is not the current module right after starting the system, it is imported by the current one, CONVERSION. Thus, we can type the following, just after starting Maude:
Notice that Maude makes explicit the module in which the term is reduced, even when no module name is given by the user.
As said above, to load for example a user-defined module HELLO-WORLD for a Maude session, you can either type at the Maude prompt the whole module or simply type the following in-troduce request:
where hello-world is a text file in the current directory containing the module HELLO-WORLD.
For files specified by a bare file name, Maude also checks for files with .maude, .fm, and .obj extensions. Maude can also be told using the MAUDE_LIB environment variable about other directories to use to search for files. Thus to find a file specified in the in command, Maude searches, in order:
If the desired file is in none of these places you must type its full path name.
As for user-defined modules, user requests such as the above can either be typed at the Maude prompt or simply in-troduced with a text file containing them. In fact, many users run Maude inside an Emacs-like editor, since this provides both text editing facilities for creating Maude modules and saving them in files, and also UNIX shell interaction to start a Maude session and to in-troduce during the session modules and commands created and saved in files, as shown in Figure 2.2.
Note that text files entered in Maude can contain not only modules, but also any command. Actually, a file can contain as many modules and commands as one wishes. When entering it with an in or load command, Maude will read them one after another as if they were written at the prompt of the system. Another important issue worth pointing out is that we can write single line and multiline comments anywhere inside a module or a file. Single line comments are started by either *** or ---, and ended by the end of line. Multiline comments are started by ***( and ended by ). Parentheses must balance within multiline comments.
We maintain the following mailing lists related to Maude:
As already mentioned, bug reports should be sent to
When submitting a bug report, please include the following information:
If Maude’s output is not obviously wrong (for example, an “internal error” message), include an explanation of why the output is wrong.
If you choose to simplify the example, note that a short runtime to expose the bug is desirable. A small example text is mostly unimportant unless it is necessary to understand such example text in order to understand why Maude’s output is incorrect.
