我正在寻找 OCaml 中的用法示例来演示简单的属性或定理。
一个例子可能是，给定二叉树的 ocaml 定义，证明最大节点数是 2^(h+1)-1。
我已经找到了这种二叉树和图的例子，但没有别的……有什么建议或链接吗？
如果您说的是写在纸上的证明，则其用法与其他语言的用法基本相同:基于程序语义的合理(但未正式化)模型的非正式推理。为了处理你的情况，我会写两个函数 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 一个)足够同步，您可以 transfer results 来证明一些 OCaml 端更改是正确的。 同样，有一些尝试为经过认证的编程设计语言，在某些领域，这些语言可能比 Coq 等通用定理证明器更方便。 Why3 就是这样一个“软件验证平台”:它定义了一种编程语言(离 OCaml 不远)和一种规范语言。您可以制定有关程序的断言并使用各种技术验证它们，例如通用证明助手(例如 Coq)或更自动化的定理证明器(SMT 求解器)。 Why3 努力支持经典命令式算法实现的验证，但也支持函数式编程风格，因此如果您不想使用完整的 Coq(例如，如果您想进行认证编程的实验)，它可能是一个有趣的选择'对确保算法终止不感兴趣，这在 Coq 中可能不方便)。 最后，已经在以下技术上进行了工作:读取您的 OCaml 程序并从中自动生成“Coq 描述”，您可以使用该属性来保证您证明正确的内容也适用于 OCaml 实现。这是 Arthur Charguéraud's 2010 PhD thesis 的主要结果，其中“Coq 描述”基于“特征公式”技术。他已经能够证明相对复杂的算法(例如 Union-Find 或 Chris Okasaki 出色的“纯函数数据结构”一书中的示例)的正确 ML 实现。 (我经常提到 Coq 证明助手；Isabelle 和 Agda 等其他工具同样适用，但 Coq 在语法上更接近 OCaml 语言，因此如果您想重新实现 ML 程序以正式证明它们，这可能是一个不错的选择正确的。)