4

我正在寻找 OCaml 中的用法示例来演示简单的属性或定理。一个例子可能是，给定二叉树的 ocaml 定义，证明最大节点数是 2^(h+1)-1。

我已经为二叉树和图表找到了这样的例子，但没有别的了..有什么建议或链接吗？

4

1 回答 1

14

如果您说的是写在纸上的证明，则其用法与其他语言基本相同：基于程序语义的合理（但未形式化）模型的非正式推理。为了处理您的情况，我将编写两个函数size和height，并通过对树的归纳推理证明，size h <= pow 2 (height h + 1) - 1在两个子树上使用归纳假设——我可以使这个解释更详细，但如果你愿意，我更愿意让你自己做。

如果你想要更正式的证明，有几种方法。

  • 基于 hoare 逻辑的证明技术已经适用于函数式编程语言。例如，参见 Régis-Gianas 和 Pottier 的 2008 年工作，A Hoare logic for call-by-value functional programs。它们为可以使用的东西提供了正式的基础，仍然以手写证明的形式，为您的主张提供更严格的（因为深入浅出）证明。它也可以用于定理证明器，但我不确定这种方法是否已经完全解决。

  • 另一种自然的方法是直接在Coq证明助手中编写程序，其编程语言主要是 OCaml 的纯函数子集，并使用其工具进行证明。这与用 OCaml 编写并不完全一样，但非常接近；那么你可以直接在 OCaml 中镜像实现，或者使用 Coq 的提取工具来获取已经从 Coq 程序“编译”的看起来很诚实的 OCaml 代码。此方法已用于形式化 OCaml 标准库中存在的平衡二叉树的实现，并且两种实现（OCaml 一种和 Coq 一种）充分同步，您可以传输结果以证明某些 OCaml 端更改是正确的.

  • 同样，有一些尝试为认证编程设计语言，在某些领域，这些语言可能比 Coq 等一般定理证明器更方便。为什么3就是这样一个“软件验证平台”：它定义了一种编程语言（离OCaml不是很远）和一种规范语言在它之上。您可以制定有关您的程序的断言并使用各种技术验证它们，例如通用证明助手（例如 Coq）或更自动化的定理证明器（SMT 求解器）。Why3 努力支持经典命令式算法实现的验证，但也支持函数式编程风格，因此如果您不想使用完整的 Coq（例如，如果您'对确保终止您的算法不感兴趣，这在 Coq 中可能很不方便）。

  • 最后，对以下技术进行了研究：阅读您的 OCaml 程序并从中自动生成“Coq 描述”，您可以对其进行属性化，并保证您证明正确的内容也适用于 OCaml 实现。这是Arthur Charguéraud 2010 年博士论文的主要成果，其中“Coq 描述”基于“特征公式”技术。他已经能够证明相对复杂的算法的正确 ML 实现，例如 Union-Find 或 Chris Okasaki 出色的“Purely Functional Data Structures”书中的示例。

（我经常提到 Coq 证明助手；Isabelle 和 Agda 等其他工具同样适用，但 Coq 在语法上更接近 OCaml 语言，因此如果您想重新实现 ML 程序以正式证明它们，这可能是一个不错的选择正确的。）

于 2012-10-18T08:18:54.510 回答