THIS PAGE IS NOT MAINTAINED. FOR THE LATEST VERSION OF FULL MAUDE GO TO THE FULL MAUDE'S GITHUB SITE.
This site contains the latest version of Full Maude. If you
are looking for the Maude system or information on it, please go to the
Maude official site.
During the development of the Maude system we have put special
emphasis on the creation of metaprogramming facilities to allow the
generation of execution environments for a wide variety of languages
and logics. The first most obvious area where Maude can be used as a
metalanguage is in building language extensions for Maude itself. Our
experience in this regard is very encouraging.
Full Maude is an extension of Maude written in Maude itself. Full Maude
adds notation for object-oriented programming, parameterized views,
module expressions specifying tuples of any size, etc. Although the
Maude distribution has included the specification/implementation of
Full Maude since it was first distributed in 1999, Core Maude and Full
Maude are now closer than ever before. Many of the features now
available in Core Maude, like parameterized modules, views, and module
expressions like summation, renaming and instantiation, were available
in Full Maude long before they were available in Core Maude. In fact,
Full Maude has not only been a complement to Core Maude, but also a
vehicle to experiment with new language features. Once these features
have been mature enough to be implemented in the core language, we have
made the effort to do so. Similarly, it is very likely that those
features in Full Maude which are not yet available in Core Maude will
become part of it sooner or later, and that new features will be added
to Full Maude for purposes of language design and experimentation.
Full Maude implements a complete user interface for the extended
language. Using the META-LEVEL and LOOP-MODE modules, we have been able
to define in Core Maude all the additional functionality required for
parsing, evaluating, and pretty-printing modules in the extended
language, and also for input/output interaction. Thanks to the
efficient implementation of the Maude rewrite engine, the parser, and
the META-LEVEL module, such a language extension executes with
reasonable efficiency.
For details on how to use the Maude system, and Full Maude,
see the
Maude
manual.
- July 13th, 2012 (Full Maude 2.6.1e)
- This version fits several bugs, being the main one a bug in the elimination of identity attributes.
- March 20th, 2012 (Full Maude 2.6.1)
- Core Maude views are now accessible from Full Maude. Full Maude do not require explicit sort maps any more.
- The
set of more general eqs and rls (moreGeneralEqs and moreGeneralRls ops)
is now correctly calculated. These functions are used in several
places, for example, in the functions and commands to eliminate
identity attributes and in the completion procedures. Reported by S.
Escobar.
- July 13th, 2011 (Full Maude 2.6b)
- This version works with Maude 2.6.
- September 11th, 2009 (Full Maude 2.4m)
- This version works with alpha92.
- Some cleaning up.
- May 13th, 2009 (Full Maude 2.4k)
- Fixed a bug in the id-unify command. Fixed by S. Escobar.
- April 18th, 2009 (Full Maude 2.4j)
- The metadata attribute is now available for operation declarations. Reported by A. Riesco.
- Fixed bug in the handling of ditto. ctor and metadata attributes were copied.
- March 9th, 2009 (Full Maude 2.4i)
- Fixed a bug in the search command. The number of solutions argument was used as depth bound. Reported by P. Olveczky.
- Fixed a bug in the handling of mbs/cmbs. Sorts in bubbles were not handled correctly. Reported by T. Serbanuta.
- The summation module expression now generates a module
fmod A + B + C is
inc A .
inc B .
inc C .
endfm
for a module expression A + B + C.
- Fixed a bug in the id-unify command. Fixed by S. Escobar.
- January 29th, 2009 (Full Maude 2.4d)
- The
downModule operation has been extended to be able to handle
object-oriented metamodules. Note that omod metamodules are defined in
the UNIT Full Maude module. Therefore, to be able to do things like
(load omod ... endom .)
the current module must be the Full Maude UNIT module or one extending it.
- A bug in downAttr. Found thanks to a problem with metamodule load. Reported by Peter Olveczky.
- January 8th, 2009 (Full Maude 2.4c)
- A bug in the narrowing functionality. It was narrowing on frozen positions. (fixed by Santiago Escobar)
- December 28th, 2008 (Full Maude 2.4b)
- Fixed a bug in the handling of the such-that part of
search commands. Reported by Enrique
Martín.
- A new search_~>_ family of commands (as for
search_=>_)
is now available. The commands are implemented by Santiago Escobar.
- December 8th, 2008 (Full
Maude 2.4a)
- A new meta-module load command is available. It enters
a
metamodule into Full Maude's database of modules. Requested by Peter
Olveczky and José Meseguer.
The syntax for the new command is (load <meta-module> .),
where
<meta-module is any term of sort Module, either a term of the
form
fmod...endfm or any other expression reducing to a module. Thus, you
can write things like
(select META-LEVEL
.)
(load fmod 'FOO is
including 'BOOL .
sorts 'Foo .
none
op 'f : nil -> 'Foo [none] .
op 'g : nil -> 'Foo [none] .
none
eq 'f.Foo = 'g.Foo [none] .
endfm .)
or
(load upModule('NAT, true) .)
Notice that the command only works if the current module imports
META-LEVEL.
Please, send any comments or
questions to |
08/12/2008 |