Formally Verifying Dynamic Properties of Knowledge Based Systems(19)

Secondly,KIVperformscorrectnessmanagement,keepingtrackofwhichproofsaredependentonwhichothers(theso-calledlemma-graph).KIValsokeepstrackofwhichproofobligationshavealreadybeenful lledornot,takingthesedependenciesintoaccount.Furthermore,itcalculateswhichproofsmustberedonewhenpartsofspeci cationsandimplementationsarechanged.

Thirdly,KIVisveryuser-friendlyandeasytolearn(certainlyincomparisonwithotherinteractivetheoremprovers).Importantfeaturesareitsgraphicaluser-interface(e.g.proofsdisplayedastrees,whichcanbeusedforproof-navigation,proof-replayandre-use,proof-cut-and-paste),itsuseofnaturalmathematicalnotationinbotheditinganddisplayingformulae,andtheproductionofpretty-printedspeci cations,programsandproofs.

5.3Summaryandconclusions

Inthispaperwehaveshownhowdespiteitslimitations,DynamicLogiccanbefruitfullyusedtoexpressandprovedynamicpropertiesofproblemsolvingmethods.Thiscouldbedonebyencodingdynamicpropertiesofthesemethodsasfunctionalpropertiesofslightlymodi edmethods.Thesemodi cationsweresmallandsystematic,sothattheadditionalencodingeffortremainedsmall.

Wehaveillustratedourapproachintwocasestudies.Inthe rstweprovedany-timebehaviourofasimplelinear lteringmethod,andinthesecondweanalyseditsbehaviourduringcomputationwhenaheuristiccandidate-selectionfunctionwasem-ployed.

Alltheproofobligationsforthesemethods(termination,correctness,dynamicbe-haviour)havebeenful lledviamachineassistedproofsusingtheKIVinteractiveveri- erforDynamicLogic.