Using correctness-by-construction to derive dead-zone algorithms

B.W. Watson, L.G. Cleophas, D.G. Kourie

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Citation (Scopus)
28 Downloads (Pure)

Abstract

We give a derivation, in the form of a stepwise (refinement-oriented) presentation, of a family of algorithms for single keyword pattern matching, all based on the so-called dead-zone algorithm-style, in which input text parts are tracked as either unprocessed (‘live’), or processed (‘dead’). Such algorithms allow for Boyer-Moore-style shifting in the input in two directions (left and right) instead of one, and have shown promising results in practice. The algorithms are the more interesting because of their potential for concurrency (multithreading). The focus of our algorithm family presentation is on correctness-arguments (proofs) accompanying each step, and on the resulting elegance and efficiency. Several new algorithms are described as part of this algorithm family, including ones amenable to using concurrency.
Original languageEnglish
Title of host publicationProceedings of the Prague Stringology Conference 2014, Prague, Czech Republic, September 1-3, 2014
EditorsJ. Holub, J. Žďárek
Place of PublicationPrague
PublisherPrague Stringology Club
Pages84-95
Number of pages12
Publication statusPublished - 2014
Externally publishedYes
EventPrague Stringology Conference 2014 - Department of Theoretical Computer Science, Czech Technical University, Prague, Czech Republic
Duration: 1 Sep 20143 Sep 2015

Conference

ConferencePrague Stringology Conference 2014
CountryCzech Republic
CityPrague
Period1/09/143/09/15

Fingerprint

Pattern matching

Cite this

Watson, B. W., Cleophas, L. G., & Kourie, D. G. (2014). Using correctness-by-construction to derive dead-zone algorithms. In J. Holub, & J. Žďárek (Eds.), Proceedings of the Prague Stringology Conference 2014, Prague, Czech Republic, September 1-3, 2014 (pp. 84-95). Prague: Prague Stringology Club.
Watson, B.W. ; Cleophas, L.G. ; Kourie, D.G. / Using correctness-by-construction to derive dead-zone algorithms. Proceedings of the Prague Stringology Conference 2014, Prague, Czech Republic, September 1-3, 2014. editor / J. Holub ; J. Žďárek. Prague : Prague Stringology Club, 2014. pp. 84-95
@inproceedings{d1d61e9b5aef463882a32992eb52d981,
title = "Using correctness-by-construction to derive dead-zone algorithms",
abstract = "We give a derivation, in the form of a stepwise (refinement-oriented) presentation, of a family of algorithms for single keyword pattern matching, all based on the so-called dead-zone algorithm-style, in which input text parts are tracked as either unprocessed (‘live’), or processed (‘dead’). Such algorithms allow for Boyer-Moore-style shifting in the input in two directions (left and right) instead of one, and have shown promising results in practice. The algorithms are the more interesting because of their potential for concurrency (multithreading). The focus of our algorithm family presentation is on correctness-arguments (proofs) accompanying each step, and on the resulting elegance and efficiency. Several new algorithms are described as part of this algorithm family, including ones amenable to using concurrency.",
author = "B.W. Watson and L.G. Cleophas and D.G. Kourie",
year = "2014",
language = "English",
pages = "84--95",
editor = "J. Holub and J. Žď{\'a}rek",
booktitle = "Proceedings of the Prague Stringology Conference 2014, Prague, Czech Republic, September 1-3, 2014",
publisher = "Prague Stringology Club",

}

Watson, BW, Cleophas, LG & Kourie, DG 2014, Using correctness-by-construction to derive dead-zone algorithms. in J Holub & J Žďárek (eds), Proceedings of the Prague Stringology Conference 2014, Prague, Czech Republic, September 1-3, 2014. Prague Stringology Club, Prague, pp. 84-95, Prague Stringology Conference 2014, Prague, Czech Republic, 1/09/14.

Using correctness-by-construction to derive dead-zone algorithms. / Watson, B.W.; Cleophas, L.G.; Kourie, D.G.

Proceedings of the Prague Stringology Conference 2014, Prague, Czech Republic, September 1-3, 2014. ed. / J. Holub; J. Žďárek. Prague : Prague Stringology Club, 2014. p. 84-95.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Using correctness-by-construction to derive dead-zone algorithms

AU - Watson, B.W.

AU - Cleophas, L.G.

AU - Kourie, D.G.

PY - 2014

Y1 - 2014

N2 - We give a derivation, in the form of a stepwise (refinement-oriented) presentation, of a family of algorithms for single keyword pattern matching, all based on the so-called dead-zone algorithm-style, in which input text parts are tracked as either unprocessed (‘live’), or processed (‘dead’). Such algorithms allow for Boyer-Moore-style shifting in the input in two directions (left and right) instead of one, and have shown promising results in practice. The algorithms are the more interesting because of their potential for concurrency (multithreading). The focus of our algorithm family presentation is on correctness-arguments (proofs) accompanying each step, and on the resulting elegance and efficiency. Several new algorithms are described as part of this algorithm family, including ones amenable to using concurrency.

AB - We give a derivation, in the form of a stepwise (refinement-oriented) presentation, of a family of algorithms for single keyword pattern matching, all based on the so-called dead-zone algorithm-style, in which input text parts are tracked as either unprocessed (‘live’), or processed (‘dead’). Such algorithms allow for Boyer-Moore-style shifting in the input in two directions (left and right) instead of one, and have shown promising results in practice. The algorithms are the more interesting because of their potential for concurrency (multithreading). The focus of our algorithm family presentation is on correctness-arguments (proofs) accompanying each step, and on the resulting elegance and efficiency. Several new algorithms are described as part of this algorithm family, including ones amenable to using concurrency.

M3 - Conference contribution

SP - 84

EP - 95

BT - Proceedings of the Prague Stringology Conference 2014, Prague, Czech Republic, September 1-3, 2014

A2 - Holub, J.

A2 - Žďárek, J.

PB - Prague Stringology Club

CY - Prague

ER -

Watson BW, Cleophas LG, Kourie DG. Using correctness-by-construction to derive dead-zone algorithms. In Holub J, Žďárek J, editors, Proceedings of the Prague Stringology Conference 2014, Prague, Czech Republic, September 1-3, 2014. Prague: Prague Stringology Club. 2014. p. 84-95