A Foundation for Verified Software Development Sys

AFoundationforVerifiedSoftwareDevelopmentSystemsChristophKreitzFachgebietIntellektik,FachbereichInformatik,TechnischeHochschuleDarmstadtAlexanderstraße10,D–64283Darmstadt,Germanyphone:[phone]e-mail:[e-mail]–94–07,TechnischeHochschuleDarmstadt,FBInformatik,FGIntellektik,1994.AbstractWedescribeaformalizationofthemeta-mathematicsofprogramminginahigher-ordercalculusasameanstocreateverifiablycorrectimplementationsofprogramsynthesistools.Formaldefinitionsandlemmataareusedtoraisethelevelofabstractioninformalreasoningtoonecomprehensibleforprogrammers.Formalmeta-theoremsmakeexplicitthesemanticknowledgecontainedinprogramderivationmethodsandserveaskernelofderivedinferencerulesimplementingthesemethods.Byanexampleformalizationofastrategyderivingglobalsearchalgorithmswedemonstratetheadvantagesofcombiningformalmathematicswithaninteractivetheoremprovingenvironmenttodeveloppowerful,flexible,andreliablesystemsforknowledge-basedsoftwaredevelopment.Keywords:ProgramSynthesis,DerivedInferences,AbstractFormalReasoning,TypeTheory1IntroductionFormorethantwentyyearscommercialsoftwareproductionhasbeeninastateofendemiccrisis.Thecrisisiscausedbytheverypropertywhichmakessoftwareattractive:thecomplexityofbehaviorthatcanbeproduced.Itcontinuesbecausethecomplexityofsoftwaregrowsfasterthanthedevelopmentoftechniquesdealingwithit.Itseffectsmanifestthemselvesintwoways.Thefirstisthecostofsoftwareoveritslifecyclewhichhasbeenemphasizedbythesharpfallinthecostofhardware.Contrarytothelatterthecostofsoftwareproductionisalmostallinthedesign,anexpensivetaskrequiringcreativity,expertise,intelligence,anddiscipline.Thesecondeffectisalackofconfidenceinsoftware.Sincecurrentsoftwareengineeringtechniquescannotprovidestringentguaranteesonsoftwarereliabilityonlyveryfewcomputerusersbelievethattheirsoftwareiscorrect.Suchconcernslimittheextenttowhichdigitalcontrolisadoptedinsafety-criticalareassuchasaircraftandnuclearreactors.Morereliablemethodssupportingthedevelopment,maintenance,andmodificationofsoftwarewouldthereforeimmediatelyfindapplicationindevelopingtheseeconomicallyimportantsystems.Attemptstoelaboratesuchtechniqueshavebeenundertakensincetheupcomingofthesoftwarecrisis.Methodologistshavewrittenabouttheart[Knu68,Knu72,Knu75],discipline[Dij76],craft[Rey81],andscience[Gri81]ofprogrammingasmeansfortheproductionofbettersoftware.Toalargeextentprogramminghasbeenidentifiedasareasoningprocessonthebasisofknowledgeofvariouskinds,anactivityinwhichpeopletendtodoalotofmistakes.Thereforeitisdesirabletoprovidemachinesupportforsoftwaredevelopmentandtodeveloptoolsforknowledgebasedsoftwareengineering.Besidesobtaininganaccuratestatementoftherequirementsthismeanssynthesizingcomputercodefromformalspecifications.Giventhefactthatcomputerizedreasoningcanhandleonlyformalobjectsthisrequiresaformalizationofallkindsofprogrammingknowledge.Researchinthefieldofprogramsynthesisisactiveintwoareas:investigationsintologicalcalculiwhichsupportaformalizationofprogrammingknowledgeandsynthesisstrategieswhich,makinguseofsuchformalizedknowledge,generateprogramsfromspecifications.1Manyformalcalculiwhicharesufficientlyexpressiveforreasoningaboutallkindsofspecificationsandprogramshavebeendevelopedduringthepastyears(seee.g.[ML84,CAB+86,GLT89,CH88]).Theyare–atleastintheory–powerfulenoughtoexpressallofmathematicsandprogramming.Butthereremainsaproblemofexpressivenessinpracticalapplications.Sincereasoningisboundtotheapplicationofelementaryinferencerulesprogramderivationsinthesecalculiareverylonganddifficulttocomprehend.Itisalmostimpossibleforahumanprogrammertoguideformalderivations.Fullyautomaticproofproceduresforsuchexpressivecalculi,however,cannotexist.Therefore,lessrigorousmethodsareusedinmanyapproachesimplementedduringthelastdecades(seee.g.[Gre69,MW79,MW80,Bib80,SL90]).Fromapracticalpointofviewtheyaremoresuccessful.TheKIDSsystem[SL90,Smi91,SP93]isbelievedtobeclosetothepointwhereitcanbeusedforroutineprogramming.Neverthelesssuchsystemscannotprovideaguaranteeforthecorrectnessofthesoftwaretheyproduce.Althoughtheirfoundationshavebeenthoroughlyinvestigatedonpaperitisnotcleartowhatextendtheimplementedsystemsreflectthesefoundations.Theyareencoded“adhoc”ratherthansystematicallyandtherearenotoolsforcheckingtheirproperties.Asaconsequence,programsynthesissystemstendtohavethesameproblemsasconventionalsoftware:onlyspecialistsareabletohandlethemproperly,unexpectederrorsoccur,andafterawhiletheybecomedifficulttomaintainandmodify(c.f.experiencesreportedin[NFK89]).Mostresearchersarepainfullyawareoftheseinadequaciesbutfeartheamountoflabournecessarytoovercomethem.Sofarthemostfruitfulapproachbridgingthegapbetweenformaldeductionandcomplexapplicationsseemedtobethatoftactics,firstintroducedinEdinburghLCF[GMW79],andsinceadoptedinmanyothersystems(seee.g.[Pau87,CAB+86,Pau89,Bun89,HRS90]).Tacticsaremeta-programsguidingtheapplicationofinferencerulesandserveasdeductionrulescombiningtheadvantagesofformalitywiththoseofhigh-levelmethods.Intrulycomplexapplications,however,theytendtobecomeveryslows