在 Coq 中对涉及全局状态效应的程序性质进行形式化验证
计算机科学中的逻辑
2013-10-15 v2 编程语言
摘要
命令式语言的语法并未显式提及状态，而其指称语义必须提及它。在本文中，我们提出了一个在 Coq 中验证操纵全局状态效应的程序性质的框架。这些性质在一个接近语法的证明系统中表达，如同在效应系统中一样，即状态不显式出现在操纵它的表达式的类型中。相反，状态通过添加到项和等式上的装饰出现。因此，在该系统中，程序的证明呈现两个方面：性质可以“至效应为止”进行验证，或者将效应纳入考量。因此，我们的 Coq 库的设计反映了这两个方面：我们的框架以两个归纳依赖类型的构造为中心，一个用于至效应为止的项，另一个用于装饰的操纵。
引用
@article{arxiv.1310.0794,
title = {Formal verification in Coq of program properties involving the global state effect},
author = {Jean-Guillaume Dumas and Dominique Duval and Burak Ekici and Damien Pous},
journal= {arXiv preprint arXiv:1310.0794},
year = {2013}
}