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 and the output trace is read into ):

*function check(, )
for each rule in the
= the pre-condition
= the post-condition
= the condition
= the counter-rule property
= 0
while true
= search(, , )
if is empty then
break
else
= the last position of the match in
if is not empty
replace(, )
if is not satisfied then
continue
replace(, )
if ( and search(, , 0) is not empty) or
(not and search(, , 0) is empty) then
output an error and exit
return successful
function search(, , )
search regular expression in starting from position
if the pattern is found then
return the matching with the value of all the groups in the pattern
else
return empty
function replace(, )
= 0
while number of groups in
replace all the citations of group in with the actual value of group
= + 1
*