Language Design in Maude

By: on June 5, 2006

I have been intrigued by Maude 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, the Sufficient Completeness Checker (SCC) and the Maude Termination Tool (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, in particular this paper and this code. 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, 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
.

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 and it draws on recent research in Modular Structural Operational Semantics, and Maude’s MSOS Tool.

The Maude manual and 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.

FacebookTwitterGoogle+

Comment

  1. Johan Van Biesen says:

    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 !

Post a comment

Your email address will not be published.

*

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>