Logic based program synthesis and transformation

ThisvolumecontainsselectedpapersofLOPSTR2000,theTenthInternational 1 WorkshoponLogic-basedProgramSynthesisandTransformation. Inadep- turefrompreviousyears,LOPSTR2000constitutedtheProgramDevelopment streamatCL2000,theFirstInternationalConferenceonComputationalLogic, heldatImperialCollege,London,on24-28July2000. ThismeantthattheLOPSTR2000ProgramCommitteewasalsotheCL2000 ProgramCommitteeforProgramDevelopment,andassuchhadtherespon- bilityforallProgramDevelopmentsubmissionstoCL2000,inadditiontothe usualLOPSTRabstracts. Asaresult,therewere18talksattheworkshop,with 2 fourpapersappearingintheproceedingsofCL2000, and14abstractsinthe 3 LOPSTR2000pre-proceedings. Inthisvolumewehavepapersbasedontenof theabstracts.^ So,paradoxically,thisvolumeisslimmerthanpreviousLOPSTRproce- ings,whilstthisyear’sProgramCommitteehavehadtodealwithmoresubm- sionsandmorecategoriesthanusual!Myheartfeltthanksgotoallthemembers oftheProgramCommitteefortheirhardandconscientiousworkinreviewing andselectingthe papersatvariousstages. Iwouldalsoliketo thankallthe additionalreviewersfortheire?ortsandprofessionalism. FororganizingCL2000,IwouldliketothanktheconferencechairMarek Sergot,theprogramchairJohnLloyd,andthelocalorganizersFrankKriwaczek andFrancescaToni. Theire?ortswerepivotalforthesuccessofCL2000. Finally, I would like to thank all the authors who submitted papers and alltheworkshopattendees. Yourcontinuedsupportiscrucialtothefutureof LOPSTR. ThenextLOPSTRworkshopwillbeheldinCyprus,withICLP2001 andCP2001. ItwillmarkthetenthanniversaryofLOPSTR,soIhopetosee manyofyouthere! March2001 Kung-KiuLau 1 http://www. cs. man. ac. uk/~kung-kiu/lopstr 2 J. W. Lloyd,V. Dahl,U. Furbach,M. Kerber,K. -K. Lau,C. Palamidessi,L. M.^ - reira,Y. Sagiv,P. Stuckey,editors,ComputationalLogic—CL2000,LectureNotes inArti?cialIntelligence 1861, Springer-Verlag,2000. 3 K. -K. Lau,editor, Pre-Proceedings of the Tenth International Workshop on Log- basedProgramSynthesisandTransformation, Technical Report UMCS-00-6-1, - partment of Computer Science, University of Manchester, June 2000. ISSN 1361- 6161. (Electronic version at: http://www. cs. man. ac. uk/cstechrep/Abstracts/ UMCS-00-6-1. html.^ ) Program Chair Kung-KiuLau UniversityofManchester,UK Program Committee DavidBasin Albert-Ludwigs-Universit¨atFreiburg,Germany AnnalisaBossi Universit`aCa’FoscaridiVenezia,Italy AntonioBrogi Universit`adiPisa,Italy MauriceBruynooghe KatholiekeUniversiteitLeuven,Belgium MireilleDucass´e IRISA/INSA,France SandroEtalle UniversiteitMaastricht,TheNetherlands PierreFlener UppsalaUniversity,Sweden MichaelHanus Christian-Albrechts-Universit¨atzuKiel,Germany IanHayes UniversityofQueensland,Australia ManuelHermenegildo TechnicalUniversityofMadrid,Spain PatriciaHill UniversityofLeeds,UK BaudouinLeCharlier UniversityofNamur,Belgium MichaelLeuschel UniversityofSouthampton,UK MichaelLowry NASAAmesResearchCenter,USA AliMili WestVirginiaUniversity,USA TorbenMogensen UniversityofCopenhagen,Denmark AlbertoPettorossi UniversityofRomeTorVergata,Italy DonSannella UniversityofEdinburgh,UK DougSmith KestrelInstitute,USA ZoltanSomogyi UniversityofMelbourne,Australia Additional Referees JamieAndrews^ IanGreen Germ´anPuebla AlessandroAvellone DavidHemer OlivierRidoux YvesBekkers BrahimHnich DaveRobertson FranciscoBueno EdKazmierczak SabinaRossi NicolettaCocco ZeynepK?z?ltan SalvatoreRuggieri RobertColvin ElviraPino JudithUnderwood MauroFerrari MaurizioProietti Germ´anVidal Table of Contents Synthesis AFormalFrameworkforSynthesisandVeri?cationofLogicPrograms . . . . . . 1 AlessandroAvellone,MauroFerrariandCamilloFiorentini ProtocolsbetweenProgramsandProofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 ImanPoernomoandJohnN. Crossley ATechniqueforModularLogicProgramRe?nement. . . . . . . . . . . . . . . . . . . . . . . 38 RobertColvin,IanHayesandPaulStrooper Transformation Higher-OrderTransformationofLogicPrograms . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 SilvijaSeresandMichaelSpivey Analysis Non-transformationalTerminationAnalysisofLogicPrograms, BasedonGeneralTerm-Orderings. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .^ . . . . . . . 69 AlexanderSerebrenikandDannyDeSchreye Specialisation AModelforInter-moduleAnalysisandOptimizingCompilation. . . . . . . . . . . 86 FranciscoBueno,Mar´?aGarc´?adelaBanda,ManuelHermenegildo, KimMarriott,Germ´anPueblaandPeterJ. Stuckey MeasuringtheE?ectivenessofPartialEvaluation inFunctionalLogicLanguages. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103 ElviraAlbert,SergioAntoyandGerm´anVidal AutomatedStrategiesforSpecializingConstraintLogicPrograms . . . . . . . . . 125 FabioFioravanti,AlbertoPettorossiandMaurizioProietti Abstract Interpretation MeasuringthePrecisionofAbstractInterpretations. . . . . . . . . . . . . . . . . . . . . . . 147 AlessandraDiPierroandHerbertWiklicky VIII TableofContents Debugging SpecifyingPrologTraceModelswithaContinuationSemantics . . . . . . . . . . . 165 ErwanJahier,MireilleDucass´eandOlivierRidoux Author Index. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .^ . . . . . . . . . . . . . . . .