Lightweight Program Construction and Verification Tools in Isabelle/HOL
Lightweight Program Construction and Verification Tools in Isabelle/HOL
复制标题
Isabelle/HOL 中的轻量级程序构建和验证工具
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
G. Struth
中科院分区：
文献类型：
--
作者：
A. Armstrong;Victor B. F. Gomes;G. Struth
我们提出了一种原则性的方法，用于开发构建和验证工具的过程。我们的验证工具使用Kleene代数和测试来捕获程序的控制流及其数据流的关系语义。它通过向代数添加一个单个公理来扩展到摩根风格的程序构建工具。我们在Isabelle/Hol中的形式化使这些工具本身可以通过构造正确。验证条件生成和程序构建步骤基于简单的方程推理，并由强大的伊莎贝尔策略支持。有关计划构建和验证的两个案例研究表明我们的工具正在工作。
We present a principled approach to the development of construction and verification tools for while-programs. Our verification tool uses Kleene algebra with tests to capture the control flow of programs and its relational semantics for their data flow. It is extended to a Morgan-style program construction tool by adding one single axiom to the algebra. Our formalisation in Isabelle/HOL makes these tools themselves correct by construction. Verification condition generation and program construction steps are based on simple equational reasoning and supported by powerful Isabelle tactics. Two case studies on program construction and verification show our tools at work.