论文标题
结合谓词变压器语义的效果：用普通语言解析的案例研究
Combining predicate transformer semantics for effects: a case study in parsing regular languages
论文作者
论文摘要
本文介绍了如何使用谓词变压器语义来验证功能编程语言中的正则表达式的解析器，以产生各种效果。 如果我们以前在该领域的工作集中在语义上以产生单一效果，则需要分析的效果组合：非确定性，一般递归和可变状态。 众所周知，关于这种效果组合的推理是很困难的，但是我们使用谓词变压器的方法可以仔细地分离程序语法，正确性证明和终止证明。
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.
