copyright c00836

《copyright c00836》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、BRICSBasicResearchinComputerScienceBRICSRS-99-54P.D.Mosses:FoundationsofModularSOSFoundationsofModularSOSPeterD.MossesBRICSReportSeriesRS-99-54ISSN0909-0878December1999Copyrightc1999,PeterD.Mosses.BRICS,DepartmentofComputerScienceUniversityofAarhus.Al

2、lrightsreserved.Reproductionofallorpartofthisworkispermittedforeducationalorresearchuseonconditionthatthiscopyrightnoticeisincludedinanycopy.SeebackinnerpageforalistofrecentBRICSReportSeriespublications.Copiesmaybeobtainedbycontacting:BRICSDepartmento

3、fComputerScienceUniversityofAarhusNyMunkegade,building540DK–8000AarhusCDenmarkTelephone:+4589423360Telefax:+4589423255Internet:BRICS@brics.dkBRICSpublicationsareingeneralaccessiblethroughtheWorldWideWebandanonymousFTPthroughtheseURLs:http://www.brics.

4、dkftp://ftp.brics.dkThisdocumentinsubdirectoryRS/99/54/FoundationsofModularSOS⋆PeterD.Mosses1BRICSandDepartmentofComputerScience,UniversityofAarhus,DenmarkAbstract.Anovelformoflabelledtransitionsystemisproposed,wherethelabelsarethearrowsofacategory,an

5、dadjacentlabelsincomputa-tionsarerequiredtobecomposable.SuchtransitionsystemsprovidethefoundationsformodularSOSdescriptionsofprogramminglanguages.Threefundamentalwaysoftransforminglabelcategories,analogoustomonadtransformers,areprovided,anditisshownth

6、attheirapplicationspreservecomputationsinmodularSOS.TheapproachisillustratedwithfragmentstakenfromamodularSOSforMLconcurrencyprimitives.1IntroductionSOS(structuraloperationalsemantics)isawidely-usedframeworkfordefin-ingprocessalgebras[17,e.g.]andprogra

7、mminglanguages[18,e.g.].FollowingPlotkin[30],SOShasoftenbeenpreferredtothemoreabstractframeworkofdenotationalsemantics.Thelabelledtransitionsystemsthatprovidethefoun-dationsforSOSarethemselveswell-studiedmathematicalobjects,withmajorapplicationsinsoft

8、ware(andhardware)engineering.ModularSOSisaformofSOSthatensuresahighdegreeofmodularity:thetransitionrulesforeachconstructarecompletelyindependentofthepresenceorabsenceofotherconstructsinthedescribedlanguage.Whenoneextendsorchangesthedescribedla