我正在寻找OCaml中的用法示例来演示简单的属性或定理.给定二叉树的ocaml定义的示例可以证明节点的最大数量是2 ^(h + 1)-1.
我已经为二进制树和图形找到了这样的例子,但没有别的......任何建议或链接？
gas*_*che 14
如果你说的是纸上写的证据,那么用法与其他语言的用法基本相同:基于程序语义的合理(但不是形式化)模型的非正式推理.为了处理你的情况我会写两个函数size和height,并通过在树归纳推理证明size h <= pow 2 (height h + 1) - 1,用在两个子树的归纳假设-我可以让这个解释更加详细,但宁愿让你自己做,如果你想.
如果您想要更正式的证据,有几种方法.
基于hoare逻辑的证明技术已经适用于函数式编程语言.例如,参见Régis-Gianas和Pottier的2008年工作,A值呼叫功能程序的Hoare逻辑.它们提供了一个正式的基础,可以使用,仍然是手写的证据,为您的索赔提供更严格(因为直接到金属)的证据.它也可以用在一个定理证明器中,但我不确定这种方法是否已经完全解决了.
另一种自然的方法是直接在Coq校对助手中编写程序,其编程语言主要是OCaml的纯功能子集,并使用其工具进行验证.这与写OCaml不完全相同,但非常接近; 然后你可以直接镜像OCaml中的实现,或者使用Coq的提取工具来获得从Coq程序"编译"的看起来很诚实的OCaml代码.这种方法已被用于形式化OCaml标准库中存在的平衡二叉树的实现,并且两个实现(OCaml one和Coq one)充分同步,您可以传输结果以证明某些OCaml端更改正确.
同样,有一些尝试设计用于认证编程的语言,在某些领域可能比一般的定理证明器如Coq更方便.Why3是一个"软件验证平台":它定义了一种编程语言(距离OCaml不远)和一种规范语言.您可以制定关于程序的断言,并使用各种技术验证它们,例如通用证明助手(例如Coq)或更自动化的定理证明器(SMT求解器).Why3努力支持经典命令式算法实现的验证,但也支持函数式编程风格,因此如果您不想使用完全Coq(例如,如果您),那么对于具有认证编程的实验来说它可能是一个有趣的选择'对确保终止算法不感兴趣,这在Coq中可能不方便).
最后,已经开展了以下技术的工作:阅读您的OCaml程序并自动生成一个"Coq描述",您可以保证您在OCaml实现中保证您所证明的正确性.这是ArthurCharguéraud2010年博士论文的主要成果,其中"Coq描述"基于"特征fomrulae"的技术.他已经能够证明相对复杂算法的正确ML实现,例如Union-Find或Chris Okasaki出色的"纯功能数据结构"一书中的例子.
(我经常提到Coq证明助手;其他工具如Isabelle和Agda同样适合,但Coq在语法上与OCaml语言更接近,所以如果你想重新实现ML程序来正式证明它们,那么它可能是一个很好的选择正确.)