List of Figures

2.1 Maude home page at maude.cs.illinois.edu
2.2 Running Maude inside Emacs
4.1 Confluence diagram
5.1 Coherence diagram
5.2 Graphical representation of search graph in example
6.1 Importation graph of bank modules
6.2 Importation graph of ticker modules
7.1 Hierarchy of order theories
7.2 Structure of LEX-PAIR
7.3 Importation graph of data-agents modules
8.1 Importation (protecting) graph of predefined modules
8.2 Importation graph of parameterized list and set modules
8.3 From lists to weakly sortable lists
8.4 From weakly sortable lists to sortable lists
8.5 Another version of sortable lists
10.1 Behavior of the amatchrew combinator
12.1 Importation graph of model-checking modules
12.2 Graphical representation of a Kripke structure
17.1 Importation graph of metalevel modules
17.2 Folding variant narrowing tree for the term < $ q q X Y >.
19.1 MiniMaude’s statechart.
20.1 LaTeX log of the interaction in which the module SIMPLE-NAT is entered, a term is reduced and the operations of the module are shown.
20.2 LaTeX log of the interaction in which the module SIMPLE-NAT is entered, a term is reduced and the operations of the module are shown. ASCII option on.
20.3 Interaction for the NAT-PAIR module.
20.4 LaTeX log of the interaction in Figure 20.3.
20.5 Interaction for the PRODUCT module.
20.6 LaTeX log of the interaction in Figure 20.5. It illustrates the use of the set print latex off command.
21.1 Number of rewrites and CPU time for different versions of the sorting algorithms