Chasing Bottoms: A Case Study in Program Verification in the Presence of Partial and Infinite Values
Chasing Bottoms: A Case Study in Program Verification in the Presence of Partial and Infinite Values
复制标题
追底：存在部分和无限值的程序验证案例研究
DOI：
10.1007/978-3-540-27764-4_6
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
Patrik Jansson
中科院分区：
文献类型：
--
作者：
Nils Anders Danielsson;Patrik Jansson
这项工作是在程序验证的案例研究：我们已经写了一个简单的解析器和相应的漂亮的打印机在一个非严格的函数式编程语言与解除对和功能（Haskell）。一个自然的目标是证明这些程序在某种意义上是彼此的逆。域中部分值和无穷值的存在使得这个练习很有趣，并且提升类型为任务增加了额外的乐趣。我们以不同的方法处理这个问题，这是一份关于这些方法优点的报告。更具体地说，我们首先描述了一种方法，用于测试程序中存在的部分和无限值的属性。通过在证明之前进行测试，我们避免了浪费时间去证明无效的陈述。然后，我们证明，我们写的程序实际上（或多或少）逆使用第一不动点归纳法，然后近似引理。
This work is a case study in program verification: We have written a simple parser and a corresponding pretty-printer in a non-strict functional programming language with lifted pairs and functions (Haskell). A natural aim is to prove that the programs are, in some sense, each others' inverses. The presence of partial and infinite values in the domains makes this exercise interesting, and having lifted types adds an extra spice to the task. We have tackled the problem in different ways, and this is a report on the merits of those approaches. More specifically, we first describe a method for testing properties of programs in the presence of partial and infinite values. By testing before proving we avoid wasting time trying to prove statements that are not valid. Then we prove that the programs we have written are in fact (more or less) inverses using first fixpoint induction and then the approximation lemma.