Formally Verifying Dynamic Properties of Knowledge Based Systems(16)

2.Introduceadditionaloutputparameter(s)forthetrace:Thesemanticchoicemadeinthepreviouspointmustbeencodedsyntacticallybymodifyingtheoriginalprogram.Thisamountstoaddingcodetotheoriginalalgorithmplusadditionaloutputparameterstoreturntheresultsofthisextracode.Inourexample,theboxedlineinFig.3re ectsthedecisiontomodelonlytheclass-selectionstep.Thechoiceofmodellingthehistory-sequenceisre ectedbytheuseofalistforthetraceparameter(insteadofaset).

3.Introduceauxiliaryprogramsforadditionaloutputparameters:Asexplainedabove,auxiliaryprogramsareneededtoside-stepthetechnicallimitationsthatspeci cationsareexpressedinfunctionalterms,andthereforeallowonlyoneout-putparameter(inourexampletheprogramsfilter-trace-1#and-2#).

4.Introduceconservationaxioms:Newaxiomsarerequiredtoenforcethattheorig-inaloutputwillnotbeaffectedbytheadditionalcode(axiom(7)above).

5.Introducebehaviouraxioms:Asa nalstep,addaxiomsthatrepresentthedy-namicpropertiesoftheoriginalprogram.Inourexamplethesewereaxioms(8)–

(10):theoriginalfilter#programconsidersthecandidateclassesindecreasingorderoftheirheuristicvalue.Thispropertyisexpressedasafunctionalpropertyofthemodi edprogramfilter-trace#.