technology from back to front

Language Design in Maude

I have been intrigued by [Maude](http://maude.cs.uiuc.edu/) for a few
years. Recently I finally found the time to play with it.

Introduction
————

Maude is quite different from most programming languages in both its
underlying fundamentals – rewriting logic – and surface
appearance. The first impression of Maude is of a language tailor-made
for experimenting with programming languages. As the Maude manual puts
it

> Maude should be viewed as a metalanguage, through which many
> different domain-specific languages can be easily developed.

In Maude one can define the syntax and semantics of programming
languages in a style that is very close to what is found in the
literature on programming language research. Crucially these
specifications are *executable*, so one ends up with fully functioning
interpreters. These interpreters perform quite well, thanks to Maude’s
efficient and tunable implementation of rewriting logic. Furthermore,
programs written in the newly defined languages can be analysed by
generic tools such as the [LTL model
checker](http://maude.cs.uiuc.edu/papers/abstract/EMSltl_2002.html),
the [Sufficient Completeness Checker
(SCC)](http://maude.cs.uiuc.edu/tools/scc/) and the [Maude Termination
Tool (MTT)](http://www.lcc.uma.es/~duran/MTT/), or bespoke tools
written specifically for the designed languages by exploiting Maude’s
reflective capabilities.

A great example of just how close Maude programs can be to formal
specifications is the [CCS case
study](http://maude.cs.uiuc.edu/maude1/casestudies/ccs/), in
particular [this
paper](http://maude.cs.uiuc.edu/papers/abstract/VMccs_2002.html)
and [this
code](http://maude.cs.uiuc.edu/maude1/casestudies/ccs/ccs2.maude). The
concision is impressive; 110 lines to define the syntax and the
semantics – in two flavours – of CCS and another 90 lines to define a
Hennesy-Milner logic model checker for it.

Another example, showing how the same approach can be employed to
build complex applications, is the [Pathway Logic
Assistant](http://www.csl.sri.com/users/clt/PLweb/), a domain-specific
language for modelling and reasoning about biological entities and
processes.

Initial experiments
——————-
I downloaded the Linux x86 binary distribution. Installation was
smooth though I wish there was a Debian package for it. I also tried
to build Maude from the source distribution. This turned out to be a
somewhat more complicated affair since it requires the presence of a
few libraries, some of which are not available as Debian
packages.

As an example I chose a variant of the [Reflective Higher Order
Process
Calculus](http://www.lshift.net/news.20050725reflectivecalculus).
Here’s what I came up with:

mod RHO is

sorts Process Name .

op # : -> Process [ctor] .
op _|_ : Process Process -> Process [ctor frozen assoc comm prec 50] .
op _!_ : Name Name -> Process [ctor frozen] .
op _?_._ : Name Name Process -> Process [ctor frozen format (d d ! o d d)] .
op ^_ : Name -> Process [ctor frozen format (d ! o)] .
op [_] : Process -> Name [ctor frozen] .

sort Subst .

op {_/_} : Name Name -> Subst [ctor] .
op __ : Process Subst -> Process [prec 40] .
op __ : Name Subst -> Name [prec 40] .

vars P Q : Process .
vars x y z z’ : Name .
var s : Subst .

eq P | # = P .

eq # s = # .
eq (x ! y)s = (x s) ! (y s) .
ceq (x ? y . P)s = x s ? y . P if {z’ / z} := s /\ z == y .
ceq (x ? y . P)s = x s ? y . P s if {z’ / z} := s /\ z =/= y .
ceq (^ x){[P] / z} = P if x == z .
eq (^ x){[P] / z} = ^ x [owise] .
eq [P]s = [P s] .
eq (P | Q)s = P s | Q s .

rl [comm] : x ? y . P | x ! z => P{z / y} .

endm

Some of the syntax may look like line noise, but that’s more due the
language I am defining than Maude itself ;). Overall the above is very
close to the syntax and semantics defined in the paper except of
course for the variations I introduced deliberately.

The first set of operator declarations defines the abstract and
concrete syntax of the language. Note that all operators are declared
as constructors, which is a hint to the system that there are ground
terms in the language which contain these operators and cannot be
further reduced. This is useful in debugging and theorem proofing. The
`frozen` attribute indicates that rewrite rules should not be applied
to sub-terms. In common with most process algebras our example
language only allows reductions at the top-level, and that’s what
`frozen` enforces. I also stuck some `format` attributes on some of
the operators. These control layout and colouring of terms in Maude’s
output. In the example the introduction and use of variables will
appear as bold.

The second set of operators defines variable substitution. This is
followed by a bunch of variable declarations and a single equation for
defining `#` as the unit of `|`. I had previously tried to define
this using an `id` attribute on the operator, but for some reason that
caused non-termination problems and also led SCC astray. This is
particularly puzzling since the use of these attributes instead of the
equivalent equations is supposed to *avoid* termination issues.

The rest of the equations define variable substitution. Notice the use
of the `:=` match construct in the conditional equations, which I
employed solely to avoid some minor code duplication.

Finally, the reduction rules of the process algebra are defined in a
single rewrite rule.

Here are some examples of equational rewrites and proper reductions:

Maude> red ([^[#]]![#]){[[#]![#]] / [#]} .
reduce in RHO : ([^ [#]] ! [#]) {[[#] ! [#]] / [#]} .
rewrites: 6
result Process: [[#] ! [#]] ! [#]

Maude> red ([#]?[#] . ^[#]){[[#]![#]] / [#]} .
reduce in RHO : ([#] ? [#] . ^ [#]) {[[#] ! [#]] / [#]} .
rewrites: 4
result Process: [#] ? [#] . ^ [#]

Maude> red ([#]?[[#]![#]] . ^[#]){[[#]![#]] / [#]} .
reduce in RHO : ([#] ? [[#] ! [#]] . ^ [#]) {[[#] ! [#]] / [#]} .
rewrites: 7
result Process: [#] ? [[#] ! [#]] . [#] ! [#]

Maude> rew [#]?[#] . ^[#] | [#]![[#]![#]] .
rewrite in RHO : [#] ! [[#] ! [#]] | [#] ? [#] . ^ [#] .
rewrites: 3
result Process: [#] ! [#]

Maude> rew [#]?[#] . (^[#] | [#]?[#] . ^[#]) | [#]![[#]![#]] .
rewrite in RHO : [#] ! [[#] ! [#]] | [#] ? [#] . (^ [#] | [#] ? [#] . ^ [#]) .
rewrites: 11
result Process: #

Conclusions
———–

Defining a little language turned out to be very easy indeed thanks to
Maude’s user-definable syntax and data types, and the sophisticated
pattern-matching and rewriting capabilities. One major strength of
Maude as a DSL development environment is that languages can be
defined in a *modular* fashion – something which I haven’t shown in my
little example. This allows programming language development to
proceed incrementally and compositionally. For the interested reader,
this particular aspect of Maude is explained in [The Rewriting Logic
Semantics
Project](http://fldit-www.cs.uni-dortmund.de/~peter/RewLogPL2.pdf) and
it draws on recent research in [Modular Structural Operational
Semantics](http://www.brics.dk/~pdm/ModularSOS.html), and Maude’s
[MSOS Tool](http://maude-msos-tool.sourceforge.net/index.html).

The Maude [manual](http://maude.cs.uiuc.edu/maude2-manual/) and
[primer](http://maude.cs.uiuc.edu/primer/) are excellent, doing a good
job of being both accessible to beginners and containing many details
for the expert reader.

Development in Maude is very interactive, via Maude’s REPL which also
features a debugger, tracer and profiler. These tools helped me to
quickly track down some silly novice errors in my language
definition. Some further trouble spots were identified by SCC, which
basically checks that the equations cover all the cases. I also tried
MTT, to check for confluence and termination, but couldn’t get it to, er, terminate.

The most serious problem I encountered in my experiments is occasional
crashes. Some of them I tracked down to non-terminating rewrites. The
Maude manual points out that this is to be expected, which seems like
a strange design decision – since it is easy to accidentally enter a
very deep or infinite rewrite sequence, surely Maude should catch this
type of error and recover from it. Some of the others crashes were
just plain mysterious and elusive and I find them quite surprising,
given that Maude has been under active development and use for several
years.

I also discovered that the Maude parser can be rather unforgiving and
produce obscure error messages. Maude doesn’t stack up too badly in
this regard compared to other language implementations, but there is
certainly room for improvement.

A related problem I ran into is that the syntax isn’t
quite as flexible as one would like. For example, most tokens require
surrounding whitespace. This not only affects the Maude grammar
itself, where one can get used to it, but also all user-defined
syntaxes, where it can become quite a nuisance that forces expressions
to be written with unnatural amounts of spacing.

While on the topic of syntax, let me mention one final annoyance: The
emacs mode for Maude required tweaking to get it to work at all, it
has hardly any indentation and expression navigation support, and
syntax-highlighting seems partially broken. It is still usable, but as
far as I can tell it hasn’t been updated for years and is in dire need
of attention.

Overall though I am quite pleased with Maude. As a DSL development
tool it is a lot of fun to work with and one gets results very
quickly. I am in the process of conducting some more experiments and
will report my findings here.

by
matthias
on
05/06/06
  1. Johan Van Biesen
    on 05/07/06 at 12:04 pm

    Recently, the MOMENT group has released an Eclipse plugin for Maude. It is a valuable alternative for the emacs mode.
    It should be used with the 1.5 release of Java !

 
 


1 × nine =

2000-14 LShift Ltd, 1st Floor, Hoxton Point, 6 Rufus Street, London, N1 6PE, UK+44 (0)20 7729 7060   Contact us