A Complete Mechanization of Correctness of a String-Preprocessing Algorithm

We report on mechanization of a correctness proof of a string-preprocessing algorithm. This preprocessing algorithm is employed in Boyer-Moore’s pattern matching algorithm. The mechanization is carried out using the PVS system. The correctness proof being mechanized has been formulated in Linear Time Temporal Logic. It consists of fourteen lemmata which are related to safety properties and two additional lemmata dealing with liveness properties. The entire mechanization of the safety and liveness parts has been completed. Several small errors and omissions were found in the handwritten proof and corrected. Yet, the manual correctness proof of the string-preprocessing algorithm was found to satisfy the usual mathematical validity. We conclude that the string-preprocessing algorithm in Boyer-Moore’s pattern matching algorithm, corrected a number of times because of flaws, does not contain any more undiscovered errors. An extended abstract of this work appears in the Proceedings of the 8^th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS ‘02).