A fast pattern matching algorithm derived by transformational and assertional reasoning

Highly optimised algorithms are, in general, hard to understand. This is a consequence of the designer's sacrifice of clarity and modularity in favour of efficiency. In this paper we present a formal derivation of a rather ingenious algorithm, viz., the fast pattern matching algorithm of Boyer and Moore. The development illustrates that transformational programming combined with assertional reasoning provides an appropriate approach for developing and understanding highly optimised algorithms.This research has been carried out within the NFT-project STOP (Specification and Transformation Of Programs) and partially sponsored by NWO (Netherlands Organisation for Scientific Research) under grant NFI-FW3315.