Using Maude?
Manuel Cla el1, F ansisco Du ´an2, S e en Eke 2, Pa ick Lincoln2,
Na ciso Ma ´ı-Olie 3, Jose Mesegue 2,andJoseF.Quesada
4
1Depa men o Philosophy, Uni e si y o Na a e, Spain
2SRI In e na ional, Menlo Pa k, CA 94025, USA
3Facul ad de Ciencias Ma em´a icas, Uni e sidad Complu ense, Mad id, Spain
4CICA (Cen o de In o m´a ica Cien ´ı ica de Andaluc´ıa), Se ille, Spain
Maude is a wide-spec um e lec i e logical language based on ew i ing logic [7]
ha can be used o speci y, p o o ype, and o mally analyze concu en so -
wa e sys ems, speci ica ion languages, logics, and heo em p o e s. Because o
i s e icien implemen a ion, i can also be used as a p og amming language and
as a me a- ool o gene a e o he ools. This pape gi es a b ie in oduc ion o
he language and illus a es wi h examples some o he ea u es o he cu en
e sion, a ailable ee o cha ge oge he wi h examples, documen a ion, and
pape s om SRI: see h p://maude.csl.s i.com. The key cha ac e is ics o
Maude can be summa ized as ollows:
–Based on ew i ing logic. This makes i pa icula ly well sui ed o exp ess
concu en and s a e-changing aspec s o sys ems decla a i ely.
–Wide-spec um. Rew i ing logic is a logical and seman ic amewo k o bo h
speci ica ion and e icien execu ion.
–Mul ipa adigm. Since ew i ing logic conse a i ely ex ends equa ional logic,
an equa ional s yle o unc ional p og amming is na u ally suppo ed in a
sublanguage. A decla a i e s yle o concu en objec -o ien ed p og amming
is also suppo ed wi h a simple logical seman ics.
–Re lec i e. Rew i ing logic is e lec i e [4, 1]. The design o Maude capi alizes
on his ac o suppo a no el s yle o me ap og amming wi h e y powe ul
module-combining and module- ans o ming ope a ions ha su pass hose
o adi ional pa ame e ized p og amming.
–In e nal S a egies. The s a egies con olling he ew i ing p ocess can be
de ined by ew i e ules and can be easoned abou inside he logic [4, 5, 1].
Maude’s implemen a ion has been designed wi h he explici goals o sup-
po ing execu able speci ica ion and o mal me hods applica ions, o being easily
ex ensible, and o suppo ing e lec i e compu a ions. Al hough i is an in e -
p e e , i s ad anced semicompila ion echniques suppo lexibili y and ace-
abili y wi hou sac i icing he pe o mance o up o 1.665 million ew i es pe
second in he ee heo y and be ween 131 housand, and 1 million ew i es pe
second i associa i i y and commu a i i y axioms a e used, on a 500MHz Alpha.
?Suppo ed h ough Rome Labo a o ies con ac F30602-97-C-0312, by DARPA and
NASA h ough Con ac NAS2-98073, by O ice o Na al Resea ch Con ac N00014-
96-C-0114, and N00014-99-C-0198.
A Decision P ocedu e o Bands
Bands a e idempo en semig oups. Deciding he wo d p oblem o bands is a
sub le p oblem, since he nai e app oach o using he idempo ency equa ion
as a s ing ew i ing ule yields a noncon luen sys em. The Maude module
below speci ies he con luen and e mina ing equa ional sys em p oposed by
Siekmann and Szabo [8]. The sub le pa is ha , e en hough he ules a e
s ing ew i ing ules applied modulo associa i i y, he added condi ional ule
has o compa e se s o elemen s in app op ia e subs ings. Thus, in addi ion
oaso Lis wi h an associa i e conca ena ion ope a o , we also need an
auxilia y so Se wi h an associa i e and commu a i e union ope a ion and
an idempo ency equa ion. This illus a es Maude’s suppo o ew i ing modulo
equa ional axioms. All combina ions o associa i i y, commu a i i y, and le and
igh iden i y a e suppo ed.
mod ASSOC-IDP is p o ec ing QID .
so s Lis Se . subso s Qid < Lis Se .
op __ : Lis Lis -> Lis [assoc] . *** lis conca ena ion
op _,_ : Se Se -> Se [assoc comm] . *** se union
op {_}: Lis -> Se . *** se o a lis
a I : Qid . a S : Se . a s L P Q : Lis .
eq S,S = S . eq L L = L . *** se and lis idempo ence
ceqLPQ=LQi {L}== {Q}and {LP}== {L}.
eq {I}=I. eq{IL}=I,{L}.
end m
We can hen decide he equali y o wo gi en wo ds by equali y, e.g.,
educe ’a ’b ’c == ’a ’b ’c ’b ’a ’b ’c
I is no di icul o see ha bo h wo ds a e educ ions, using he idempo ency
equa ion as a ule, om he common ances o ’a ’b ’a ’b ’c ’b ’a ’b ’c.
Re lec ion and he META-LEVEL
Rew i ing logic is e lec i e [4, 1] in he p ecise sense ha he e is a ini ely
p esen ed ew i e heo y Usuch ha o any ini ely p esen ed ew i e heo y T
(including Ui sel ) we ha e he ollowing equi alence
T` −→ 0⇐⇒ U`hT, i−→hT, 0i
whe e Tand a e e ms ep esen ing Tand as da a elemen s o U. In Maude e-
lec ion is e icien ly suppo ed h ough i s p ede ined META-LEVEL module, which
p o ides key unc ionali y o he uni e sal heo y U. In pa icula , META-LEVEL
has so s Te m and Module, whose espec i e e ms a e me a ep esen a ions and
T, o e m and Ta module ( ha is, a ew i e heo y). Fo example, a e m
= (a,g(b)), in a module FOO,wi ha,bcons an s o so Foo is me a ep e-
sen ed as =’ [{’a}Foo,’g[{’b}Foo]].META-LEVEL has a numbe o unc ions
o pe o ming me ale el compu a ions in he uni e sal heo y [2]. In pa icula ,
he me a-apply unc ion applies a he me ale el a ule in a module o a e m.
I s ope a o decla a ion is
op me a-apply : Module Te m Qid Subs i u ion MachineIn -> Resul Pai .
The i s and second a gumen s a e me a ep esen a ions T,and o a module
Tand a e m ; he hi d a gumen is he label o he ule, he ou h is a
subs i u ion ins an ia ing some a iables in he ule, and he i h is a numbe
indica ing he ma ch ins ance wi h which we wan o ew i e. Since ma ching
may be pe o med modulo axioms such as associa i i y, commu a i i y and/o
iden i y, in gene al a ule may ma ch a subjec e m in se e al di e en ways. The
esul o applying he unc ion is a pai , consis ing o he (me a ep esen a ion
o ) he ew i en e m and he ma ching subs i u ion in case o success, o an
e o cons an and he emp y subs i u ion in case o ailu e.
A Re lec i e Example
The ollowing example demons a es he use o he Maude me ale el. The ex-
ample consis s o de ining a me ale el unc ion indAllRew i es ha , gi en
a e m in a module T, will ind ( he ep esen a ion o ) all one-s ep ew i es
om .No e ha me a-apply only applies a ule a he op o he subjec e m,
whe eas he e we wan all one-s ep ew i es a all e m posi ions.
mod META is p o ec ing META-LEVEL .
so Te mSe . subso Te m < Te mSe .
a T : Te m . a S : Subs i u ion . a L : Qid .
a s TL Be o e A e : Te mLis . a s OP SORT : Qid .
a N : MachineIn . op i s : Resul Pai -> Te m .
op ~ : -> Te mLis . eq ~, TL = TL . eq TL, ~ = TL . op {} : -> Te mSe .
op _|_ : Te mSe Te mSe -> Te mSe [assoc comm id: {}].
op me a-apply1 : Te m Qid MachineIn -> Te m .
op indAllRew i es : Te m Qid -> Te mSe .
op indTopRew i es : Te m Qid MachineIn -> Te mSe .
op indLowe Rew i es : Te m Qid -> Te mSe .
op ew i eA gumen s : Qid Te mLis Te mLis Qid -> Te mSe .
op ebuild : Qid Te mLis Te mSe Te mLis -> Te mSe .
eq me a-apply1(T, L, N) = i s (me a-apply([’FOO], T, L, none, N)) .
eq T | T = T . eq i s ({T, S})=T.
eq indAllRew i es(T, L) = indTopRew i es(T, L, 0) | indLowe Rew i es(T, L) .
eq indTopRew i es(T, L, N) = i me a-apply1(T, L, N) == e o * hen {}
else me a-apply1(T, L, N) | indTopRew i es(T, L, N + 1) i .
eq indLowe Rew i es({OP}SORT, L) = {} .
eq indLowe Rew i es(OP[TL], L) = ew i eA gumen s(OP, ~, TL, L) .
eq ew i eA gumen s(OP, Be o e, T, L) = ebuild(OP, Be o e, indAllRew i es(T, L), ~) .
eq ew i eA gumen s(OP, Be o e, (T, A e ), L) =
ebuild(OP, Be o e, indAllRew i es(T, L), A e ) |
ew i eA gumen s(OP, (Be o e, T), A e , L) .
eq ebuild(OP, Be o e, {}, A e ) = {} .
eq ebuild(OP, Be o e, T, A e ) = OP[Be o e, T, A e ] .
eq ebuild(OP, Be o e, (T | TS), A e ) = (OP[Be o e, T, A e ]) |
ebuild(OP, Be o e, TS, A e ) .
end m
Gi en a module FOO wi h only one ule labeled ’one, he ollowing inds all
one s ep ew i es om (a, g(b)).
educe indAllRew i es(’ [{’a}Foo,’g[{’b}Foo]], ’one).
Applica ions
Maude is a wide-spec um language and an a ac i e o mal me a- ool o build-
ing many ad anced applica ions and o mal ools. Subs an ial applica ions in-
clude: a module sys em o Maude implemen ed in Maude [6], an induc i e
heo em p o e ; a Chu ch-Rosse checke (bo h pa o a o mal en i onmen
o Maude and o he Ca eOBJ language [3]); an HOL o Nup l ansla o ; a
p oo assis an o he Open Calculus o Cons uc ions (OCC); and a ansla o
om J. Millen’s CAPSL speci ica ion language o he CIL in e media e lan-
guage. In addi ion, se e al language in e p e e s and s a egy languages, se e al
objec -o ien ed speci ica ions—including c yp og aphic p o ocols and ne wo k
applica ions—and a a ie y o execu able ansla ions mapping logics, a chi ec-
u al desc ip ion languages and models o compu a ion in o he ew i ing logic
e lec i e amewo k ha e been de eloped by di e en au ho s.
We hank e e yone on he Maude eam o hei con ibu ions o he sys em
and his pape . We hank ou colleagues wo king on simila sys ems such as
Ca eOBJ and ELAN o in e es ing discussions and help ul commen s.
Re e ences
[1] Manuel Cla el. Re lec ion in gene al logics and in ew i ing logic, wi h applica ions
o he Maude language. Ph.D. Thesis, Uni e si y o Na a e, 1998.
[2] Manuel Cla el, F ancisco Du ´an, S e en Eke , Pa ick Lincoln, Na ciso Ma ´ı-Olie ,
Jos´e Mesegue , and Jos´e Quesada. Maude: speci ica ion and p og amming in ew i -
ing logic. SRI In e na ional, Janua y 1999, h p://maude.csl.s i.com.
[3] Manuel Cla el, F ancisco Du ´an, S e en Eke , and Jos´e Mesegue . Build-
ing equa ional p o ing ools by e lec ion in ew i ing logic. In P oc. o
he Ca eOBJ Symposium ’98, Numazu, Japan. Ca eOBJ P ojec , Ap il 1998.
h p://maude.csl.s i.com.
[4] Manuel Cla el and Jos´e Mesegue . Re lec ion and s a egies in ew i ing logic. In
J. Mesegue , edi o , P oc. Fi s In l. Wo kshop on Rew i ing Logic and i s Applica-
ions, olume 4 o Elec onic No es in Theo e ical Compu e Science. Else ie , 1996.
h p://www.else ie .nl/cas/ ee/s o e/ cs/ ee/noncas/pc/ olume4.h m.
[5] Manuel Cla el and Jos´e Mesegue . In e nal s a egies in a e lec i e logic. In
B. G amlich and H. Ki chne , edi o s, P oceedings o he CADE-14 Wo kshop on
S a egies in Au oma ed Deduc ion (Towns ille, Aus alia, July 1997), pages 1–12,
1997.
[6] F ancisco Du ´an. A e lec i e module algeb a wi h applica ions o he Maude
language. Ph.D. Thesis, Uni e si y o Malaga, 1999.
[7] Jos´e Mesegue . Condi ional ew i ing logic as a uni ied model o concu ency.
Theo e ical Compu e Science, 96(1):73–155, 1992.
[8] J. Siekmann and P. Szabo. A noe he ian and con luen ew i e sys em o idempo-
en semig oups. Semig oup Fo um, 25:83–110, 1982.