All About Maude - A High-Performance Logical Framework

How to Specify, Program, and Verify Systems in Rewriting Logic


By
  • M. Clavel, Universidad Complutense de Madrid, Spain;
  • F. Durán, Universidad de Málaga, Spain;
  • S. Eker, SRI International, Menlo Park, CA, USA;
  • P. Lincoln, SRI International, Menlo Park, CA, USA;
  • N. Martí-Oliet, Universidad Complutense de Madrid, Spain;
  • J. Meseguer, University of Illinois at Urbana-Champaign, Urbana, IL, USA;
  • C. Talcott, SRI International, Menlo Park, CA, USA

This monograph gives a comprehensive account of Maude, a language and system based on rewriting logic. Maude and its formal tool environment can be used in three mutually reinforcing ways: as a declarative programming language, as an executable formal specification language, and as a formal verification system. Maude is used in many institutions around the world for teaching, research, and formal modeling and analysis of concurrent and distributed systems. Many examples are used throughout the book to illustrate the main ideas, features, and uses of Maude. The book comes with a CD-ROM containing the complete Maude 2.3 software distribution (including source code), a pdf version of this monograph, and the executable Maude code for all the examples in the book.... more from Springer.

Known typos in the book

  • In page 163, "behaviour" should be spelled as "behavior".
  • At the end of page 182, the equation 

      eq initial
        = sq(1,1,b) sq(1,2,w) sq(1,3,w) sq(1,4,w) ...
           ... sq(8,5,w) sq(8,6,w) sq(8,7,w) sq(8,8,b) .

    should be

      eq initial
        = sq(1,1,w) sq(1,2,b) sq(1,3,b) sq(1,4,b) ...
          ... sq(8,5,b) sq(8,6,b) sq(8,7,b) sq(8,8,w) .

    The b's and w's must be interchanged so that it matches the description at the beginning of the section: Imagine an 8 × 8 board where the four corners are colored white and all the other squares are black.
  • In page 217, the last equation of the POLYNOMIAL module is

        eq A ++ B = A ++ B .

    It should be

        eq A ++ B = A + B .
  • In pages 423 and 438, there are some sorts and operators related to TermList and CTermList that were correct at the time of writing, but have become outdated with respect to the latest release of Maude. The updated description can be found in version 2.4 of the Maude manual and in the prelude.maude file in the Maude distribution.
  • In page 432, the result of the first reduce command in Section 14.4.2 should be

      result ResultPair:
        {'_._['s_^2['0.Zero], 's_^3['0.Zero], 's_^5['0.Zero],
              's_^7['0.Zero], 's_^11['0.Zero], 's_^13['0.Zero],
              's_^17['0.Zero], 's_^19['0.Zero], 's_^23['0.Zero],
              's_^29['0.Zero]],
         'NatList}

    instead of

      result ResultPair:
        {’_._[’s_^2[’0.Zero], ’s_^3[’0.Zero], ’s_^5[’0.Zero],
              ’s_^7[’0.Zero], ’s_^11[’0.Zero], ’s_^13[’0.Zero],
              ’s_^17[’0.Zero], ’s_^19[’0.Zero], ’s_^23[’0.Zero],
              ’s_^29[’0.Zero]],
         ’IntList}

    Note that the sort of the resulting term must be 'NatList, and not 'IntList.
  • In page 463, section 15.3, there are two mistakes in the DEADLOCK-FREEDOM module (a corrected version of the module can be found in the current set of files):
    • For each operator f : k1 ... kn -> k, an equation 
          enabled(f(x1, ..., xi, ..., xn)) = true if enabled(xi)
      must be generated, for 1 <= i <= n; when n = 0, no equation should be generated.
    • Equations on polymorphic operations are tricky. In the case of enabled, we are interested only on the positive cases; however, given polymorphic operators like if_then_else_fi or _==_, we must generate equations for each possible kind. All combinations are now generated for Universal arguments.
  • In the first line of page 608, in the 8-PUZZLE module, the declaration of the messages left, right, up, and down must begin with the keyword msgs instead of ops.
 more typos or comments to duran[at]lcc[dot]uma[dot]es