Improvements in program synthesis using fine-grain

IFIPWG2.1,WorkingConf.onConstructingProgramsfromSpecications,May91,PacicGrove/CAImprovementsinProgramSynthesisUsingFine-GrainSortedLogicyJochenBurghardtGMDForschungsstelleanderUniversitatKarlsruhe(GermanNationalResearchCenterforComputerScience)Vincenz-Prienitz-Strae1,D-7500KarlsruheTel.:*49-721-662245E-Mail:[e-mail]:Thispaperintroducesanewconstructor-basedsortdisciplineonpredicatelogicwhichallowstoexpressmoresophisticatedsortsthanconventionalapproaches.Algorithmsaregiventocalculateinmumanddierenceoftwosortsandtodecidethesubsortandtheequivalenceproperty.Therangesortofadenedfunctioniscalculatedfromitsdeningequations,leadingtoamoreexactdescriptionthanobtainingasignaturefromtheuser:dierentequationsareusuallyassigneddierentsorts.Thus,thesortdisciplinehelpstoselectthe\rightequationsforinferencesteps,andcutsdownthesearchspaceofaformalproof.Thiseectisdemonstratedusinganexamplefromtheareaofdatarenementandimplementationproofs.1IntroductionThegrowingneedforhighqualitysoftwarerequiresmoreandmoretheapplicationoffor-malprogramdevelopmentmethods.Variousapproachestothisareaareknown,requiringformalproofsinoneoranothermathematicalframework.OneofthemainproblemscommontotheseapproachesistheenourmousextraexpenserequiredtoperformlotsofmostlytrivialproofstepsthatmakescomputersupportnecessarytondproofsatleastyThisworkwaspartiallyfundedbytheBMFTprojectKorso,contractnumberITS9001A7.forsimplesubproblems.Itisawellknownexperiencethatevenforsuchsimplesubproblemsitishardandoftenimpossibletondsolutionsautomaticallybybruteforce(topdown)search.Instead,thesuccessofmanyformalprogramdevelopmentmethodsseemstobebasedonakindof(bottomup)preparationofthe\domainofdiscourseinordertogainsomeknowledgethatcanactpartlyasasubstitutefortheintuitionofahumanprover.Finance[Fin88],forexample,usesdataowanalysisontheaxiomsandgoalsinordertodirectHornclauseresolution.Bird[Bir86]usestheformationofalgebraic(homomorphic)lawstoavoidinductioninhisproofs;thenecessaryinductionsaremostlypartofthepreparationofaspecicdomainandcanoftenbedoneonceandforall.MannaandWaldingeruseorderingrelationsandmonotonicfunctionsasaproofguidingprinciple[MaWa86,Tra89].Inthispaper,asortdisciplineisintroducedforthesamepurposeof\preparingadomain.Themoreexpressiveasortdisciplineis,themoreinformationcanbestatedintermsofsortsratherthanofformulasandthusthemoreworkcanbeshiftedfromageneralpurposetheoremprovertospecialsuitedsortcheckalgorithms.Employinganorder-sorteddiscipline,consistingofapartiallyorderednitesetofsorts,hasturnedouttoenablearesolutionprovertosolveSchubert’ssteamrollerproblem[Wal85].Recentworkcombinesorder-sortednesswiththemeansofparametricpolymor-phism[Smo89],allowingamoresophisticatedsorthierarchyduetothemonotonicityofthesortconstructors.Inconventionalapproaches,dataconstructors(likecons(x;l))arestrictlydistinguishedfromsortconstructors(likelist()).Inthispaper,ane-grainsortdisciplineisdescribedthatisbasedonviewingeachdataconstructoralsoasasortconstructor.Asaconse-quence,therecanbeinnitechainsofsortinclusions(like:::s(s(nat))s(nat)nat)whichareforbiddeneveninSmolka’sframework[Smo89];sorttermscanbearbitrarycomplex,reectingthecomplexityofdatatermsthatcanoccurduringaproof.Thus,thesortofadatatermcanbedescribedmoreprecisely.Analgorithmforcalculatingtheinmumoftwosortsispresentedthatdynamicallycreatesanewrecursivedenitionoftheinmumsort.Forexample,theevennumbersandthenaturalnumbersdivisiblebythreecanbeexpressedassortsandtheirinmumiscalculatedasthesortofnaturalnumbersdivisiblebysix.Analogously,analgorithmforcalculatingthedierenceoftwosortsisgivenwhichservesasabasisfordecidingthesubsortpropertyandhencetheequivalenceoftwosorts.Therangesortofanon-constructorfunctioniscalculatedfromitsdeningequationsratherthanbeinggivenbyadeclaration.Sortcalculationallowstodeterminetherangesortsdependingonthedomainsortsmoreprecisely,assertingpossiblydierentsortstotherighthandsidesofdierentdeningequations.Thus,equationscanbeselectedordiscardedforanactualinferencestepbyreasoningaboutsorts.Analgorithmforcalculatingtherangesortofafunctionisgiven.Thesortcalculationalgorithmsaredemonstratedusinganexamplefromtheprogramsynthesisarea,showingtheeectofsearchspacereduction.Afteramotivatingexampleinsection2andthedenitionofsyntaxandsemanticsofasortsysteminsection3,weintroducethemainalgorithmsinsections4through7.Insection8nally,weresumetheexamplefromsection2andshowhowthesortalgorithmscanbeusedtoguideprogramsynthesis.Afullversionincludingallproofscanbeobtainedfromtheauthor.2MotivationConsiderthefollowingexamplefromtheareaofformalprogramdevelopment.Weusethemethodofdatarenement(cf.forexample[Gri81,Ehr80,Nei87])tondanimplementationofnaturalnumberswhichisclosetotheecientrepresentationbybinarystringsusedincomputerhardware.WehavethesortofnaturalnumbersinPeanoformandthesortoflistsofbinarydigitsinreversenotation(\:=denotessortdenition,\jdenotestheunionofsorts):nat:=0js(nat)bin:=niljo(bin)ji(bin)Furthermore,wehaveaxiomsdeningtherepresentationfunctionvalfrombintonatandanauxiliaryfunct