The string search algorithm by Knuth, Morris and Pratt (Q7361250)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Knuth_Morris_Pratt
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | The string search algorithm by Knuth, Morris and Pratt |
AFP entry Knuth_Morris_Pratt |
Statements
18 December 2017
0 references
Fabian Hellauer
0 references
Peter Lammich
0 references
The string search algorithm by Knuth, Morris and Pratt (English)
0 references
The Knuth-Morris-Pratt algorithm is often used to show that the problem of finding a string s in a text t can be solved deterministically in O(|s| + |t|) time. We use the Isabelle Refinement Framework to formulate and verify the algorithm. Via refinement, we apply some optimisations and finally use the Sepref tool to obtain executable code in Imperative/HOL .
0 references
