Formal derivation of a pattern matching algorithm

DOI10.1016/0167-6423(89)90036-1MaRDI QIDQ1822923zbMATH OpenOpenAlexFDO

Authors Richard S. Bird, Jeremy Gibbons, Geraint Jones

Publication date 1989

Published in Science of Computer Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0167-6423(89)90036-1

zbMATH Keywords

functional programminglistspattern matchingprogram derivation

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Specification and verification (program logics, model checking, etc.) (68Q60) Algorithms in computer science (68W99)

Review text

The functional version of the Knuth-Morris-Pratt pattern matching algorithm is formally derived using the Bird's calculus of lists. The derivation process is thoroughly explained, various solving strategies are discussed, the paper is self-contained.

Recommendations

• A fast pattern matching algorithm derived by transformational and assertional reasoning
• scientific article; zbMATH DE number 30308
• Playing with patterns, searching for strings
• Derivation of a parallel string matching algorithm
• On string pattern matching: A quantitative analysis and a proposal

Cited in

(12)

• The derivation of on-line algorithms, with an application to finding palindromes
• Playing with patterns, searching for strings
• List partitions
• Formal Techniques for Deriving Binary Search Algorithms
• scientific article; zbMATH DE number 30308 (Why is no real title available?)
• Categories, relations and dynamic programming
• Proof of Correctness of a Direct Construction of DFA from Regular Expression
• scientific article; zbMATH DE number 1822176 (Why is no real title available?)
• A sheaf-theoretic approach to pattern matching and related problems
• Putting the `K' into Bird's derivation of Knuth-Morris-Pratt string matching
• Derivation of efficient logic programs by specialization and reduction of nondeterminism
• A fast pattern matching algorithm derived by transformational and assertional reasoning

This page was built for publication: Formal derivation of a pattern matching algorithm

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1822923)