Maude 2.4 release

Dear colleagues,

Maude 2.4 is now available from the Maude web-site at http://maude.cs.uiuc.edu 
.

This release includes Core Maude 2.4, Full Maude 2.4 and a new Maude  
2.4 manual.

The main new features and changes since 2.3 are listed below. Please,  
see the new manual for additional details.

Best regards,

The Maude Team


==================================
New features and changes since 2.3
==================================

(1) Maude 2.4 provides an order-sorted Ax-unification algorithm for  
all order-sorted theories (Sigma, E U Ax) such that:
   - the signature Sigma is preregular modulo Ax;
   - the axioms Ax associated to function symbols are as follows:
        - there can be arbitrary function symbols and constants with  
no equational attributes;
        - the iter equational attribute can be declared for some unary  
symbols;
        - the comm or assoc comm attributes can be declared for some  
binary function symbols, but then no other equational attributes must  
be given for such symbols.
Explicitly excluded are theories with binary function symbols having  
either: (i) the id:, left id:, or right id: attributes; or (ii) the  
assoc attribute without the comm one; or (iii) a combination of (i)  
and (ii).

(2) Unification is reflected in the META-LEVEL module by two descent  
functions:
     op metaUnify : Module UnificationProblem Nat Nat ~>  
UnificationPair? [special (...)] .
     op metaDisjointUnify : Module UnificationProblem Nat Nat ~>  
UnificationTriple? [special (...)] .

(3) Statements (rule, equations and membership axioms) can now take a  
print attribute. In print attribute mode, when a statement is executed  
the items in its print attribute are printed, with variables taking  
their value in the current substitution.

(4) Parsing of file names in the commands load, in, cd and pushd now  
allows spaces using either of two syntactic conventions:
If the file name starts with " then all following characters will be  
taken literally up to the terminating ", line feed or form feed.
If a file name starts with other than ", the following escape  
sequences are recognized
   \\          becomes \
   \<space>    becomes <space>
   \"          becomes "

(5) For operators in the C, CU, CI and CUI theories, if both arguments  
are the same, the rewrite, srewrite and search commands and the model  
checker will only consider one of the arguments for that step since  
only one rewriting step is made per pass, the choice of argument is  
irrelevant. This already happened for operators in the AC and ACU  
theories. The frewrite command still always considers all arguments  
even if they are identical since multiple rewriting steps can happen  
in each pass.

(6) The GNU libsigsegv library is used to distinguigh between true  
segmentation faults and stack overflows and so stack overflows are now  
reported with an informative message.

(7) Several optimizations, bug fixes and improvements._______________________________________________
Maude-users mailing list
Maude-users@...
http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-users