ac米兰官方网站 使用乐高定理证明器正式开发 SML 程序

引用

马哈拉吉 S (1991)使用乐高定理证明器正式开发 SML 程序。贝尔实验室。

摘要
本报告描述了使用乐高定理证明器开发 SML 程序的尝试。我们的目标是使用定理证明器作为一个统一的环境，在其中表达规范、编码实现，然后验证实现是否满足规范。特别是，我们希望利用定理证明者类型系统中的某些构造作为在规范和程序中表达模块化的机制。这项工作是在 Elsa Gunter 的监督下进行的，当时作者作为大学关系项目的参与者于 1991 年夏天访问贝尔实验室。我在乐高系统中表达了一个程序规范。然后我编写了一个机器学习程序，并将其翻译成乐高，之后我正式证明翻译后的程序满足规范。该规范描述了一个函子，该函子将一个由基本类型组成的结构作为输入，该结构在该类型的元素上具有相等关系，并返回一个由基本类型及其相等性、基于基本类型的集合类型以及对这些集合进行操作的函数集合（例如并集、交集等）组成的结构。