基于交互式与自动定理证明器支持的不变式编程练习
计算机科学中的逻辑
2012-02-23 v1 编程语言
摘要
不变式编程（IBP）是一种基于图表的“构造即正确”编程方法论，其中程序围绕不变式构建，且不变式在实际代码编写之前就已形式化。Socos 是专门为支持 IBP 而构建的程序构建与验证环境。Socos 的前端是一个图形化图表编辑器，允许程序员构建基于不变式的程序并检查其正确性。Socos 的后端组件（程序检查器）计算程序的验证条件并尝试自动证明它们。它使用定理证明器 PVS 和 SMT 求解器 Yices，在无需用户交互的情况下尽可能多地解除验证条件。在本文中，我们首先从用户和系统层面描述 Socos 环境；然后通过在 Socos 中构建一个经过验证的堆排序实现来示例 IBP 工作流程。该案例研究突出了自动和交互式定理证明在 IBP 工作流程三个连续阶段中的作用：开发背景理论、形式化程序规格说明与不变式，以及证明最终实现的正确性。
引用
@article{arxiv.1202.4829,
title = {An Exercise in Invariant-based Programming with Interactive and Automatic Theorem Prover Support},
author = {Ralph-Johan Back and Johannes Eriksson},
journal= {arXiv preprint arXiv:1202.4829},
year = {2012}
}
备注
In Proceedings THedu'11, arXiv:1202.4535