Formally Verifying Dynamic Properties of Knowledge Based Systems(13)

ccsmeasurecmeasureselectcs

Theadaptedfilter-trace#programhastwooutputparameters:traceandoutput.However,inaspeci cationafunctioncanonlyreturnoneoutput.Thistechnicalobsta-clecanbeavoidedbyintroducingtwoauxiliaryprograms:oneprogramforreturningthetraceparameter,andoneforreturningtheoutputparameter.Thetrivialimple-mentationoftheseauxiliaryprogramsisasfollows:

filter-trace-1#(cs;varoutput)

begin

vartrace=nilin

filter-trace#(cs;trace,output)

end

filter-trace-2#(cs;vartrace)

begin

/invaroutput=0

filter-trace#(cs;trace,output)

end