ACL2
ACL2（A Computational Logic for Applicative Common Lisp，应用式 Common Lisp 计算逻辑）是由一个程序语言、一套一阶逻辑的可拓理论、以及一个机械化的定理证明器所组成的软件系统。ACL2 从设计上支持基于归纳逻辑理论的自动推理，可应用于软件或硬件系统的形式化验证。ACL2 的编程语言及其实现基于 Common Lisp。ACL2 是基于BSD授权发布的开源软件。
 | |
| 编程范型 | 函数式编程、元编程 |
|---|---|
| 设计者 | 罗伯特·斯蒂芬·博伊尔 斯特罗瑟·摩尔 马特·考夫曼 |
| 实现者 | 马特·考夫曼 斯特罗瑟·摩尔 |
| 发行时间 | 1990年（内部发布） 1996年（公开发布） |
| 类型系统 | 动态类型 |
| 操作系统 | 跨平台 |
| 许可证 | BSD License |
| 网站 | ACL2 |
| 启发语言 | |
| Common Lisp、NQTHM | |
简介
ACL2 的编程语言可看作是一个函数式（无任何副作用）的 Common Lisp 变体。和 Lisp 一样，ACL2 使用动态类型系统。ACL2 中所有的函数均是完整定义的（total）——每一个函数均在 ACL2 的全集中将各个对象（输入）映射到另一个对象（输出）。
ACL2 的基础理论已将其程序语言的语义及其内建函数全部公理化。而程序语言中满足定义原则的用户自定义部分在扩展该理论的同时亦能保持其逻辑自洽性。ACL2 定理证明器的核心基于项重写系统，此核心高度可扩展，用户已证得的定理可以在后续的猜想中被用作现成的数学证明。
ACL2 设计的目标是成为 Boyer–Moore 定理证明器 NQTHM 的一个“工业级别”版本。为了达成此目标，ACL2 涵盖了支持许多数学和计算理论之工程学应用的有趣特性。ACL2 因为基于 Common Lisp 实现而继承了其高效率；作为归纳验证基础的同一规范亦可以被编译器编译及优化，进而在本地执行。
2005年，Boyer-Moore 系列定理证明器（包括 ACL2）的开发者获得了ACM软件系统奖，获奖理由是“作为最高效的定理证明器的先驱和工程师……开发了能够用于验证硬件和软件可靠性的形式化工具”。[1]
应用
ACL2 在若干领域得以应用[2][3]。 例如，在奔腾浮点除错误被曝光之后，斯特罗瑟·摩尔 和马特·考夫曼运用 ACL2 证明了 AMD K5 处理器的浮点数除法运算的正确性。[4] 在 ACL2 文档的有趣的应用[5]页面里有一些关于其实际应用的简介。
ACL2 的工业界用户包括超微半导体公司、Centaur科技、国际商业机器股份有限公司、英特尔、甲骨文公司和罗克韦尔柯林斯。
参考
- ^ Software System Award. ACM Awards. ACM. [2012]. （原始内容存档于2012-04-02）.
- ^ Books and Papers about ACL2 and Its Applications. [2014-01-24]. （原始内容存档于2013-11-06）.
- ^ The ACL2 Workshop Series. [2014-01-24]. （原始内容存档于2014-02-13）.
- ^ A mechanically checked proof of the correctness of the kernel of the AMD5K86 floating point division algorithm. CiteSeerX: 10.1.1.43.3309
.
- ^ 有趣的应用（页面存档备份，存于互联网档案馆）
