Recent Trends in Algebraic Development Techniques

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-J¨orgKreowski (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. Große-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 ¨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. Schr¨oder X TableofContents TheCommonFrameworkInitiativeforAlgebraicSpeci?cation andDevelopmentofSoftware:RecentProgress. . . . . . . . . . . . . . . . . . . . . . . . . 328 D. Sannella AuthorIndex . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 345 InteractiveRule-BasedSpeci?cationwithan ApplicationtoVisualLanguageDe?nition 1 1 2 Roswitha Bardohl , Martin Große-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 c