Defining a Formal Coalgebraic Semantics for the Ro

DefiningaFormalCoalgebraicSemanticsforTheRosettaSpecificationLanguageCindyKongandPerryAlexander(TheUniversityofKansasDeptofElectricalEngineeringandComputerScienceInformationandTelecommunicationTechnologyCenter2335IrvingHillRoadLawrence,Kansas66045{ckong,alex}@ittc.ku.edu)CatherineMenon(DepartmentofComputerScienceTheUniversityofAdelaideSA5005,[e-mail])Abstract:Rosettaisasystemsleveldesignlanguagethatallowsalgebraicspecifica-tionofsystemsthroughfacets.Theusualapproachtoformallydescribeaspecificationistodefineanalgebrathatsatisfiesthespecification.Althoughitispossibletofor-mallydescribeRosettafacetswiththeuseofalgebras,wechoosetousethedualofalgebra,i.e.coalgebra,todoso.Coalgebrasareparticularlysuitedfordescribingstate-basedsystems.Thismakesformallydefiningstate-basedRosettaquitestraightforward.Fornon-state-basedRosetta,theformalizationisnotasdirect,butcanstillbedonewithcoalgebrasbyfocusingonthebehaviorsofsystemsspecified.Weusedenota-tionalsemanticstomapRosettasyntacticconstructsintoalanguageunderstoodbythecoalgebras.KeyWords:coalgebra,state-based,systembehavior,algebraicspecification,systemleveldesignlanguage,formalsemantics,denotationalsemanticsCategory:F.1.1,F.3.2,F.4.31IntroductionAnimportantpartinthedevelopmentofanewlanguageistoformallydefinewhatthelanguagedenotes.Thisisespeciallytrueforspecificationlanguages.Formostalgebraicspecificationlanguages,theformalizationofthelanguageconsistsofdescribingthealgebrasthatsatisfyaspecification[EhrigandMahr1985].AsimilarapproachisusedintheformaldefinitionoftheRosettasystemlevelde-signlanguage.However,insteadofdefiningalgebras,coalgebras,thedualsofal-gebras,aredefined.Coalgebrasareparticularlysuitedfordescribingstate-basedsystems,consequentlyfordescribingstate-baseddomainsinRosetta.However,Rosettaisnotrestrictedtostate-basedcomputation.Indeed,oneofthemajorJournalofUniversalComputerScience,vol.9,no.11(2003),1322-1349submitted:12/6/03,accepted:5/9/03,appeared:28/11/03©J.UCSbenefitsofRosettaisitsflexibilityinallowingdifferentmodelsofcomputation,suchastrace-based,event-based,graph-basedandthelike.Thesemanticsofsystemsfromthesedifferentmodelsofcomputationcanstillbeexpressedwithcoalgebrasthatrepresenttheirbehaviors.ThelinkbetweencoalgebrasandtransitionsystemsisclearlydefinedbyAlexanderKurz[Kurz2001].Hefirstdefinesatheoryofsystemsdescribingre-lationsbetweendifferentsystems,andthendemonstrateshowcertainsystemsgiverisetocoalgebras.OuruseofcoalgebrasinformallydefiningRosettaspec-ificationsisfoundedonhiswork.Otherinsightstotherelationbetweenstate-baseddynamicalsystemsandcoalgebrasaregiveninseveralpapers.JacobsandRutten[JacobsandRutten1997]citeseveralofthemintheirtutorialon(co)algebrasand(co)induction.Ofspecialinteresttous,thattutorialdescribeshowafunctioncanbecoinductivelydefinedovercoalgebras.WeusethesameapproachtodefineextensionrelationsbetweenRosettaunitsofspecification.Rosetta[Alexanderetal.1999,AlexanderandKong2001]isasystemsleveldesignlanguagethatusesfacetsasunitsofspecification.Afacetisasignature,consistingofoperators,functionsandvariables,aswellasasetoftermsthatdefineconstraintsoverthesignature.Itisusedtospecifyaviewofasystemorcomponentintermsofsomemodelofcomputation.Thesemanticsofamodelofcomputationisdefinedinaspecialfacet,calleddomain.Afacetissaidtoextendadomainwhenitconsistentlyuses,addstoorconstrainsthedefinitionsofthatdomain.Thefacetsignatureisalsoaugmentedbythedomainsignature.Adomaincanbeanextensionofanotheronesimilarlytoafacet.Theformaldefinitionoffacetsanddomainsconsistsofdescribingcoalgebrasforthem.WeusedenotationalfunctionstomapRosettasyntaxtocoalgebrasemantics.Then,extensionsaredefinedbycoinductionoverthecoalgebraicstructuresoffacetsanddomains.Inthenextsections,weelaborateontheformalizationofthesemanticsofRosettafacetsanddomains.Wefirstpresentsomecoalgebraicdefinitionsinthebackgroundsection,derivedfrombothKurz[Kurz2001]andJacobsandRut-ten’s[JacobsandRutten1997]papers.WethenprovideageneralapproachtothedenotationofRosettafacetstocoalgebras.Thedenotationiscalledαandisdividedintotwoparts.ThefirstpartinvolvesrepresentingafacetasacoalgebraandthesecondconsistsofdenotingRosettatermsintoalanguageunderstoodbythecoalgebra.WethendescribetheformalizationofsomespecificRosettadomainsandrelationsintocoalgebraicstructures.Followingthis,anexampleofformallydefiningaRosettadomainandfacetisgiven.Thenextsectionthendescribeshowcommutingdiagramsareusedtodefinespecialfunctionsacrossdomainsthatarethenusedtodefineinteractions.Theconclusionsectionfinallycompletesthispaperwithadescriptionoffuturework.1323KongC.,AlexanderP.,MenonC.:DefiningaFormalCoalgebraicSemantics...2CoalgebraicBackgroundThissectionprovidesanoverviewofcoalgebrasandtheuseofcoalgebrasinthesemanticsofsystems.ThedefinitionsaresummarizedfromKurz’slecturenotes[Kurz2001]andJacobsandRutten’stutorial[JacobsandRutten1997]inSection2.1andSection2.2respectively.Kurzdefinesatheoryofsystemsanddescribesthesemanticsofsomesystemsascoalgebras.JacobsandRuttendefinecoalgebrasforfunctorsandusesspecialrelationshipsbetweencoalgebrastocoinductivelydefinefunctions.Ourde