Abstract
Brzozowski introduced the notion of derivatives for regular expressions. They can be used for a very simple regular expression matching algorithm. Sulzmann and Lu cleverly extended this algorithm in order to deal with POSIX matching, which is the underlying disambiguation strategy for regular expressions needed in lexers. Sulzmann and Lu have made available on-line what they call a “rigorous proof” of the correctness of their algorithm w.r.t. their specification; regrettably, it appears to us to have unfillable gaps. In the first part of this paper we give our inductive definition of what a POSIX value is and show (i) that such a value is unique (for given regular expression and string being matched) and (ii) that Sulzmann and Lu’s algorithm always generates such a value (provided that the regular expression matches the string). We also prove the correctness of an optimised version of the POSIX matching algorithm. Our definitions and proof are much simpler than those by Sulzmann and Lu and can be easily formalised in Isabelle/HOL. In the second part we analyse the correctness argument by Sulzmann and Lu and explain why the gaps in this argument cannot be filled easily.
Original language | English |
---|---|
Title of host publication | Interactive Theorem Proving |
Subtitle of host publication | 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings |
Editors | Jasmine Christian Blanchette, Stephan Merz |
Publisher | Springer |
Pages | 69-86 |
Number of pages | 18 |
ISBN (Electronic) | 9783319431444 |
ISBN (Print) | 9783319431437 |
DOIs | |
Publication status | Published - 2016 |
Event | ITP 2016: Interactive Theorem Proving - LORIA Building, Inria Nancy - Grand-Est, Nancy, France Duration: 22 Aug 2016 → 27 Aug 2016 Conference number: 7 https://itp2016.inria.fr/ |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Volume | 9807 |
ISSN (Print) | 0302-9743 |
Conference
Conference | ITP 2016: Interactive Theorem Proving |
---|---|
Abbreviated title | ITP 2016 |
Country/Territory | France |
City | Nancy |
Period | 22/08/16 → 27/08/16 |
Internet address |
Keywords
- POSIX matching
- Derivatives of regular expressions
- Isabelle/HOL