基于谓词Transformer语义的证明工程
Proof Engineering with Predicate Transformer Semantics
摘要：
我们提出了一个轻量级的，开源的Agda框架，手动验证有效的程序使用谓词Transformer语义。我们表示的抽象语法树（AST）的有效程序与广义代数数据类型（GADT）AST，其一般性，即使是复杂的操作是原始的AST节点。然后，用户可以将定制的谓词Transformers分配给这些操作，以帮助证明工作，例如通过自动分解分支代码的证明义务。我们的框架编纂和推广的证明工程方法，作者使用的理由LibraBFT，拜占庭容错共识协议，其中参与者执行的代码可能会产生的影响，如更新状态和发送消息的原型实现。在这种情况下，我们的框架的成功使用证明了它的实用性。
英文摘要：
We present a lightweight, open source Agda framework for manually verifying effectful programs using predicate transformer semantics. We represent the abstract syntax trees (AST) of effectful programs with a generalized algebraic datatype (GADT) AST, whose generality enables even complex operations to be primitive AST nodes. Users can then assign bespoke predicate transformers to such operations to aid the proof effort, for example by automatically decomposing proof obligations for branching code. Our framework codifies and generalizes a proof engineering methodology used by the authors to reason about a prototype implementation of LibraBFT, a Byzantine fault tolerant consensus protocol in which code executed by participants may have effects such as updating state and sending messages. Successful use of our framework in this context demonstrates its practical applicability.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
