Maude program/spec

Brian T Rice water@tunes.org
Tue Apr 22 20:16:02 2003


On Tue, 22 Apr 2003 m.dentico@virgilio.it wrote:
> Brian T Rice wrote:
> > To heed the recent call to actually write code, I've uploaded my toy
> > Maude executable specification to my specification uploads area:
> >
> > http://tunes.org/~water/spec/
> This is really a good news. You have preceded me, I was about to suggest
> a thing of the sort. Maude allows to have a specification short, very
> precise and even executable.

Yes, although soon I will likely benefit from defining a Maude
"sublanguage" (not really a DSL) for TUNES specifications, which would
effectively make this TUNES prototype a Maude extension.

One of the reasons for this is to support definitions of things in terms
of a different rewrite / evaluation semantics, for example to allow for
definition and proper handling of bi-directional rewrite rules.

> With a proper mix of formal specification in Maude and relatively short
> comments in English we should be able to improve the level of
> communication and in the same time have a functional prototype.

Let's hope so. Apparently people didn't grasp the concept that I could
crank this out very quickly from my english descriptions, so I put the
code out there to emphasize the reality that evades them. :) Anyway, if
this amount of precision (regardless of its accuracy in any way) makes
people feel better and want to talk, then that's what I'll provide.

> In this setting different parts of the project fit in very well; correct
> me if I'm wrong Brian: the HLL, the *Library* of objects which represent
> High-Level concepts, is available to express domain or application
> specific concepts (eventually with an ad-hoc syntax).

Yep. This was my intention from the start, and I can re-use Maude objects
and modules with a fair amount of ease... the distinction is not very
abrupt.

> Then the (meta-)translator will translate these high-level objects into
> low-level objects described in the LLL, the Low-Level *Library*. In this
> library hardware o system specific aspects are modeled.

Yes, and the LLL will be defined as HLL objects whose subject matter is
the low level.

> However which news do you have regarding Maude development? For when
> does it have esteemed the next release?

It's getting closer. The move of the web site to UIUC was a good sign at
least. The bugs are dissappearing and the code is getting cleaner, but I
don't have an estimated release date yet.

> > Let me know if this makes something more clear, less clear, or how you
> > think it could be clearer. Obviously Configurations are not really
> > specified there, so there's something to immediately bother me about.
>
> Unfortunately at the moment I have not much time to dedicate, a new job
> is approaching. But you know, I have expressed previously an interest in
> Maude (in particular, a self hosting Maude would be great, IMO) so I
> will definitely devote some time in the near future, as soon as
> possible.

I would like to see some coherent Maude code gathered into one whole, in
contrast to the scattered examples on a few research and academic sites
here and there. However, Maude's implementation needs some serious work,
since there are O(n^2) size factors for module source size in Maude 1.
However, the C++ basis has been a large factor, since "code reuse" even
among compiler components isn't very great.

-- 
Brian T. Rice
LOGOS Research and Development
mailto:water@tunes.org
http://tunes.org/~water/