Kleene Algebra with Tests and Coq Tools for while Programs
Kleene Algebra with Tests and Coq Tools for while Programs
复制标题
Kleene 代数以及用于 while 程序的测试和 Coq 工具
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
D. Pous
中科院分区：
文献类型：
--
作者：
D. Pous
我们提供了一个关于 Kleene 代数的 Coq 库，并进行了测试，包括证明它们在适当的语言概念上的完整性、方程理论的决策过程以及利用此类理论中某种假设的工具。
带测试的 Kleene 代数可以用命令式编程语言表示 if-then-else 语句和 while 循环。它们实际上是作为命题霍尔逻辑的替代品而引入的。
我们通过证明 while 程序的等价性、一些标准编译器优化的正确性、部分正确性的 Hoare 规则以及流程图方案的特别具有挑战性的等价性，展示了如何在程序验证的上下文中利用相应的 Coq 工具。
We present a Coq library about Kleene algebra with tests, including a proof of their completeness over the appropriate notion of languages, a decision procedure for their equational theory, and tools for exploiting hypotheses of a certain kind in such a theory.
Kleene algebra with tests make it possible to represent if-then-else statements and while loops in imperative programming languages. They were actually introduced as an alternative to propositional Hoare logic.
We show how to exploit the corresponding Coq tools in the context of program verification by proving equivalences of while programs, correctness of some standard compiler optimisations, Hoare rules for partial correctness, and a particularly challenging equivalence of flowchart schemes.