Using Maude

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.