组合谓词Transformer语义实现效果：解析正则语言的案例研究
Combining predicate transformer semantics for effects: a case study in parsing regular languages
摘要：
本文描述了如何使用谓词Transformer语义来验证函数式程序设计语言中正则表达式的解析器的各种效果。我们以前在这个领域的工作集中在单一效果的语义上，解析需要效果的组合：非确定性，一般递归和可变状态。推理这种组合的影响是出了名的困难，但我们的方法使用谓词Transformers，使程序语法，正确性证明和终止证明的仔细分离。
英文摘要：
This paper describes how to verify a parser for regular expressions in a functional programming language using predicate transformer semantics for a variety of effects. Where our previous work in this area focused on the semantics for a single effect, parsing requires a combination of effects: non-determinism, general recursion and mutable state. Reasoning about such combinations of effects is notoriously difficult, yet our approach using predicate transformers enables the careful separation of program syntax, correctness proofs and termination proofs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
