Recent Trends in Algebraic Development Techniques

Thealgebraicapproachtosystemspeci?cationanddevelopment,borninthe early1970sasaformalmethodforabstractdatatypes,encompassestoday,atthe beginningofthethirdmillennium,theformaldesignofintegratedhardwareand softwaresystems,newspeci?cationframeworksandprogrammingparadigms, andawiderangeofapplicationareas. TheworkshopsonAlgebraicDevelopment Techniques,initiatedin1982astheworkshoponAbstractDataTypes,area prominentforumtopresentanddiscusscurrentresearchinthatarea. The15thInternationalWorkshoponAlgebraicDevelopmentTechniques (WADT2001)tookplaceinGenova,asasatelliteofETAPS2001,onApril 1-3,2001,andwasorganizedbyMauraCerioliandGiannaReggio. From1991to1995WADTworkshopswereheldjointlywiththeGeneral WorkshopoftheESPRITBasicResearchWorkingGroupCOMPASS. Following thistradition,theWADT2001washeldjointlywiththeGeneralWorkshopof theESPRITWorkingGroupCoFI. TheCommonFrameworkInitiative,started in1995andfundedsince1998asCoFIWG,iscenteredaroundthede?nitionof theCommonAlgebraicSpeci?cationLanguage(CASL). TheprogramstartedwithafulldaytutorialontheCASL,followedby32 presentations,severalofthemontheCASLaswell,organizedinparallelsessions duringthefollowingtwodays.Theparallelsessionsweredevotedto:logicsand proofs,concurrentprocesses,institutionsandcategories,applicationsandcase studies,higher-orderandparameterizedspeci?cations,staticanalysis,software architectures,graphandtransformationrules. Themaintopicsoftheworkshopwere: -algebraicspeci?cation -otherapproachestoformalspeci?cation -speci?cationlanguagesandmethods -termrewritingandproofsystems -speci?cationdevelopmentsystems(concepts,tools,etc. ) Theprogramcommitteeinvitedsubmissionsoffullpapersforpossibleinclusion inthisvolume,onthebasisoftheabstractsandthepresentationsatWADT 2001. Allthesubmissionsweresubjecttocarefulrefereeing,andtheselectionof paperswasmadefollowingfurtherdiscussionbythefullprogramcommittee. Weareextremelygratefultoallworkshopparticipants,tothe(other)m- bersoftheprogramcommittee,andtotheexternalrefereesfortheircontribution tothescienti?cqualityoftheworkshopandofthisvolume. TheWADTseriesissponsoredbyIFIPWG1. 3onFoundationsofSystem Speci?cation(seehttp://www. brics. dk/"pdm/IFIP-WG1. 3).November2001 MauraCerioliandGiannaReggio Organization ProgramCommittee MichelBidoit (Cachan,France) MauraCerioli (Genova,Italy) Hans-JorgKreowski (Bremen,Germany) PeterMosses,chair (Aarhus,Denmark) FernandoOrejas (Barcelona,Spain) FrancescoParisi-Presicce (Roma,Italy) GiannaReggio (Genova,Italy) DonaldSannella (Edinburgh,Scotland) AndrzejTarlecki (Warsaw,Poland) ExternalReferees EgidioAstesiano ManuelKoch MarekBednarczyk MikolajKonarski BenjaminBlanc AlexanderKurz AlexandreBoisseau SabineKuske TomaszBorzyszkowski SlawomirLasota PaoloBottoni ChristophLuth .. PaoloCenciarelli DirkPattinson HartmutEhrig Wies lawPawlo wski StevenEker Jean-ClaudeReynaud JeanGoubault-Larrecq MarkusRoggenbach PiotrHo?man SponsoringInstitutions CoFI(CommonFrameworkInitiative),ESPRITWorkingGroup29432. DISI,Universit'adegliStudidiGenova. IFIPWG1. 3onFoundationsofSystemSpeci?cation. TableofContents InteractiveRule-BasedSpeci?cationwithanApplication toVisualLanguageDe?nition ...1 R. Bardohl,M. Grosse-Rhode,andM. Simeoni AlgebraicAbstractions ...21 M. BidoitandA. Boisseau CombiningLogics:ParchmentsRevisited...48 C. Caleiro,P. Mateus,J. Ramos,A. Sernadas CanonicalInstitutionsofBehaviour ...71 J. F. CostaandH.Louren,co TheLub Thealgebraicapproachtosystemspeci?cationanddevelopment,borninthe early1970sasaformalmethodforabstractdatatypes,encompassestoday,atthe beginningofthethirdmillennium,theformaldesignofintegratedhardwareand softwaresystems,newspeci?cationframeworksandprogrammingparadigms, andawiderangeofapplicationareas. TheworkshopsonAlgebraicDevelopment Techniques,initiatedin1982astheworkshoponAbstractDataTypes,area prominentforumtopresentanddiscusscurrentresearchinthatarea. The15thInternationalWorkshoponAlgebraicDevelopmentTechniques (WADT2001)tookplaceinGenova,asasatelliteofETAPS2001,onApril 1-3,2001,andwasorganizedbyMauraCerioliandGiannaReggio. From1991to1995WADTworkshopswereheldjointlywiththeGeneral WorkshopoftheESPRITBasicResearchWorkingGroupCOMPASS. Following thistradition,theWADT2001washeldjointlywiththeGeneralWorkshopof theESPRITWorkingGroupCoFI. TheCommonFrameworkInitiative,started in1995andfundedsince1998asCoFIWG,iscenteredaroundthede?nitionof theCommonAlgebraicSpeci?cationLanguage(CASL). TheprogramstartedwithafulldaytutorialontheCASL,followedby32 presentations,severalofthemontheCASLaswell,organizedinparallelsessions duringthefollowingtwodays.Theparallelsessionsweredevotedto:logicsand proofs,concurrentprocesses,institutionsandcategories,applicationsandcase studies,higher-orderandparameterizedspeci?cations,staticanalysis,software architectures,graphandtransformationrules. Themaintopicsoftheworkshopwere: -algebraicspeci?cation -otherapproachestoformalspeci?cation -speci?cationlanguagesandmethods -termrewritingandproofsystems -speci?cationdevelopmentsystems(concepts,tools,etc. ) Theprogramcommitteeinvitedsubmissionsoffullpapersforpossibleinclusion inthisvolume,onthebasisoftheabstractsandthepresentationsatWADT 2001. Allthesubmissionsweresubjecttocarefulrefereeing,andtheselectionof paperswasmadefollowingfurtherdiscussionbythefullprogramcommittee. Weareextremelygratefultoallworkshopparticipants,tothe(other)m- bersoftheprogramcommittee,andtotheexternalrefereesfortheircontribution tothescienti?cqualityoftheworkshopandofthisvolume. TheWADTseriesissponsoredbyIFIPWG1. 3onFoundationsofSystem Speci?cation(seehttp://www. brics. dk/"pdm/IFIP-WG1. 3).November2001 MauraCerioliandGiannaReggio Organization ProgramCommittee MichelBidoit (Cachan,France) MauraCerioli (Genova,Italy) Hans-JorgKreowski (Bremen,Germany) PeterMosses,chair (Aarhus,Denmark) FernandoOrejas (Barcelona,Spain) FrancescoParisi-Presicce (Roma,Italy) GiannaReggio (Genova,Italy) DonaldSannella (Edinburgh,Scotland) AndrzejTarlecki (Warsaw,Poland) ExternalReferees EgidioAstesiano ManuelKoch MarekBednarczyk MikolajKonarski BenjaminBlanc AlexanderKurz AlexandreBoisseau SabineKuske TomaszBorzyszkowski SlawomirLasota PaoloBottoni ChristophLuth .. PaoloCenciarelli DirkPattinson HartmutEhrig Wies lawPawlo wski StevenEker Jean-ClaudeReynaud JeanGoubault-Larrecq MarkusRoggenbach PiotrHo?man SponsoringInstitutions CoFI(CommonFrameworkInitiative),ESPRITWorkingGroup29432. DISI,Universit'adegliStudidiGenova. IFIPWG1. 3onFoundationsofSystemSpeci?cation. TableofContents InteractiveRule-BasedSpeci?cationwithanApplication toVisualLanguageDe?nition ...1 R. Bardohl,M. Grosse-Rhode,andM. Simeoni AlgebraicAbstractions ...21 M. BidoitandA. Boisseau CombiningLogics:ParchmentsRevisited...48 C. Caleiro,P. Mateus,J. Ramos,A. Sernadas CanonicalInstitutionsofBehaviour ...71 J. F. CostaandH.Lourencco TheLub eckTransformationSystem:ATransformationSystem forEquationalHigherOrderAlgebraicSpeci?cations ...85 W. DoschandS. Magnussen OntheCompatibilityofModelandModel-ClassTransformations ...109 M. GajewskyandF. Parisi-Presicce VerifyingaSimplePipelinedMicroprocessorUsingMaude ...128 N. A. Harman VerifyingArchitecturalSpeci?cations...152 P. Ho?man GeometricModellingwithCASL...176 F. Ledoux,A. Arnould,P. LeGall,andY. Bertrand ACompositionalApproachtoConnectorConstruction ...201 A. Lopes,M. Wermelinger,andJ. L. Fiadeiro InstitutionIndependentStaticAnalysisforCasl ...221 T. MossakowskiandB. Klin TightandLooseSemanticsforTransformationSystems...238 F. Orejas,H. Ehrig,andE. Pino PresentationsforAbstractContextInstitutions...256 W. Paw lowski Programs,ProofsandParametrizedSpeci?cations...280 I. Poernomo,J. N. Crossley,andM. Wirsing TowardsTrustworthySpeci?cationsI:ConsistencyChecks ...305 M. RoggenbachandL. Schroder X TableofContents TheCommonFrameworkInitiativeforAlgebraicSpeci?cation andDevelopmentofSoftware:RecentProgress...328 D. Sannella AuthorIndex ...345 InteractiveRule-BasedSpeci?cationwithan ApplicationtoVisualLanguageDe?nition 1 1 2 Roswitha Bardohl , Martin Grosse-Rhode , and Marta Simeoni 1 Institutfur .. SoftwaretechnikundTheoretischeInformatik,TUBerlin, {rosi,mgr}@cs. tu-berlin. de 2 DipartimentodiInformatica,Universit'aCa'FoscaridiVenezia, simeoni@dsi. unive. it Abstract. Inarule-basedapproachthecomputationstepsofasystem arespeci?edbyrulesthatcompletelyde?nehowthesystem'sstatemay change. Foropensystemsamoreliberalapproachisrequired,wherethe statechangesareonlypartlyspeci?ed,and-interactively-otherc- ponents may contribute further information on how the transformation isde?nedcompletely.