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