Putting the `K' into Bird's derivation of Knuth-Morris-Pratt string matching

Peter Gammie 🌐

August 25, 2020

Abstract

Richard Bird and collaborators have proposed a derivation of an intricate cyclic program that implements the Morris-Pratt string matching algorithm. Here we provide a proof of total correctness for Bird's derivation and complete it by adding Knuth's optimisation.

License

BSD License

Topics

Session BirdKMP

Depends on