Mercurial Mercurial > hg > lexing / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys/Paper/document/root.tex
changeset 172 cdc0bdcfba3f
parent 154 2de3cf684ba0
child 174 4e3778f4a802
equal deleted inserted replaced
171:91647a8d84a3 172:cdc0bdcfba3f 
    66 that the regular expression matches the string).  We also prove the
 
    66 that the regular expression matches the string).  We also prove the
 
    67 correctness of an optimised version of the POSIX matching
 
    67 correctness of an optimised version of the POSIX matching
 
    68 algorithm. Our definitions and proof are much simpler than those by
 
    68 algorithm. Our definitions and proof are much simpler than those by
 
    69 Sulzmann and Lu and can be easily formalised in Isabelle/HOL. In the
 
    69 Sulzmann and Lu and can be easily formalised in Isabelle/HOL. In the
 
    70 second part we analyse the correctness argument by Sulzmann and Lu and
 
    70 second part we analyse the correctness argument by Sulzmann and Lu and
 
    71 explain why it seems hard to turn it into a proof rigorous enough to
 
    71 explain why the gaps in this argument cannot be filled easily.\smallskip
 
    72 be accepted by a system such as Isabelle/HOL.\smallskip
 
       
    73 
    72 
    74 {\bf Keywords:} POSIX matching, Derivatives of Regular Expressions,
 
    73 {\bf Keywords:} POSIX matching, Derivatives of Regular Expressions,
 
    75 Isabelle/HOL
 
    74 Isabelle/HOL
 
    76 \end{abstract}
 
    75 \end{abstract}
 
    77 
    76
lexing