Skip to main content

Formal Derivation of a Pattern Matching Algorithm

Richard S. Bird‚ Jeremy Gibbons and Geraint Jones

Abstract

This paper is devoted to the synthesis of a functional version of the Knuth-Morris-Pratt algorithm for pattern matching. This algorithm was first discussed by Knuth; since then formal developments have been given by Dijkstra and Dromey, among many others. The novel aspects of the present treatment are: (i) the result is expressed as a (very short) functional program; and (ii) the derivation makes use of the calculus of lists described by Bird.

Journal
Science of Computer Programming
Month
jul
Number
2
Pages
93–104
Volume
12
Year
1989