7.3 Rule Checker

A rule checker is implemented to read in a text file with rules defined in it, and check the correctness of the output trace saved in another text file.

The algorithm of the rule checker is summarized below (suppose that the rule file is read into $rules$ and the output trace is read into $outtrace$):

function check($rules$, $outtrace$)
for each rule $r$ in the $rules$
$pre$ = the pre-condition
$post$ = the post-condition
$cond$ = the condition
$counter$ = the counter-rule property
$pos$ = 0
while true
$match$ = search($pre$, $outtrace$, $pos$)
if $match$ is empty then
break
else
$pos$ = the last position of the match in $outtrace$
if $cond$ is not empty
replace($cond$, $match$)
if $cond$ is not satisfied then
continue
replace($post$, $match$)
if ($counter$ and search($post$, $outtrace$, 0) is not empty) or
(not $counter$ and search($post$, $outtrace$, 0) is empty) then
output an error and exit
return successful

function search($re$, $text$, $pos$)
search regular expression $re$ in $text$ starting from position $pos$
if the pattern is found then
return the matching with the value of all the groups in the pattern
else
return empty

function replace($text$, $match$)
$i$ = 0
while $i$ $<$ number of groups in $match$
replace all the citations of group $i$ in $text$ with the actual value of group $i$
$i$ = $i$ + 1