Putting the `K' Into Bird's Derivation of Knuth-Morris-Pratt String Matching

Peter Gammie 🌐

August 25, 2020

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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.
BSD License

Topics

Theories of BirdKMP