ACL2

维基百科,自由的百科全书
跳转至: 导航搜索
ACL2
编程范型 函数式编程, 元编程
发行时间 1990(内部发布)
1996(公开发布)
設計者 Robert S. Boyer
J Strother Moore
Matt Kaufmann
實作者 Matt Kaufmann
J Strother Moore
最新发行时间 6.4 / 2014年1月9日(9個月前) (2014-01-09)
型態系統 动态类型
啟發語言 Nqthm, Common Lisp
作業系統 跨平台
許可證 BSD License
網站 ACL2

ACL2(A Computational Logic for Applicative Common Lisp,应用 Common Lisp 计算逻辑)是由一个程序语言、一套一阶逻辑的可拓理论、以及一个机械化的定理证明器所组成的软件系统。ACL2从设计上支持基于归纳逻辑理论的自动推理,可应用于软件或硬件系统的验证。ACL2的编程语言与实现基于 Common Lisp。ACL2是基于BSD授权发布的开源软件

ACL2程序语言可看作是一个函数式(无任何副作用)的 Common Lisp 变体。和Lisp一样,ACL2使用动态类型。ACL2中所有的函数均是完整的(total)——意即,每一个函数均在ACL2的全集中将各个对象(输入)映射到另一个对象(输出)。

ACL2的基础理论将其程序语言的语义及其内置函数全部公理化。而程序语言中满足定义原则(definitional principle)的用户自定义部分在扩展该理论的同时亦能保持其逻辑自洽性

ACL2定理证明器的核心基于项重写(term rewriting)系统,此核心高度可扩展,用户已证得的定理可以在后续的猜想中被用作现成的数学证明

ACL2设计的目标是成为 Boyer–Moore 定理证明器 NQTHM 的一个“工业级别”版本。为了达成此目标,ACL2涵盖了支持许多数学和计算理论之工程学应用的有趣特性。ACL2因为基于 Common Lisp 实现而继承了其高效率;作为归纳验证基础的同一规范亦可以被编译器编译及优化,进而在本地执行。

2005年,Boyer-Moore 系列证明器(包括 ACL2)的开发者获得了ACM软件系统奖,获奖理由是“作为最高效的定理证明器的先驱和工程师……开发了能够用于验证硬件和软件可靠性的形式化工具。”[1][2]

证明[编辑]

ACL2在若干领域得以应用。[3][4]例如,在 Pentium FDIV bug 被曝光之后,J Strother Moore 和 Matt Kaufmann 运用ACL2证明了AMD K5处理器的浮点数除法运算的正确性。[5] 在ACL2文档的有趣的应用页面里有一些关于其实际应用的简介。

ACL2的工业级用户包括了AMDCentaur TechnologyIBMIntelOracleRockwell Collins

参考[编辑]

  1. ^ ACM: Press Release, March 15, 2006
  2. ^ Software System Award. ACM Awards. ACM. [2012]. 
  3. ^ Books and Papers about ACL2 and Its Applications
  4. ^ The ACL2 Workshop Series
  5. ^ A mechanically checked proof of the correctness of the kernel of the AMD5K86 floating point division algorithm. CiteSeerX: 10.1.1.43.3309. 

外部链接[编辑]