imported>HighSierra0820：补充字词转换

2024-11-25T17:11:44Z

补充字词转换

新页面

{{NoteTA
|G1=IT
|1=zh-hans:浮点除;zh-hant:浮點除;
}}

{{Infobox programming language
| name = ACL2
| logo = ACL2 Logo 2014 transparent.png
| paradigm = [[函数式编程]]、[[元编程]]
| designer = 罗伯特·斯蒂芬·博伊尔<br>斯特罗瑟·摩尔<br>马特·考夫曼
| developer = 马特·考夫曼<br>斯特罗瑟·摩尔
| year = 1990年（内部发布）<br>1996年（公开发布）
| latest_release_version = 8.2
| latest_release_date = {{release_date|2019|05}}
| typing = [[动态类型]]
| influenced_by = [[Common Lisp]]、[[NQTHM]]
| operating_system = 跨平台
| license = [[BSD License]]
| website = [http://www.cs.utexas.edu/users/moore/acl2/ ACL2]
}}

'''ACL2'''（'''A''' '''C'''omputational '''L'''ogic for '''A'''pplicative '''C'''ommon '''L'''isp，应用式 Common Lisp 计算逻辑）是由一个[[程序语言]]、一套[[一阶逻辑]]的可拓理论、以及一个机械化的[[定理机器证明|定理证明器]]所组成的[[软件]]系统。ACL2 从设计上支持基于[[归纳逻辑]]理论的[[自动推理]]，可应用于软件或硬件系统的形式化验证。ACL2 的编程语言及其实现基于 [[Common Lisp]]。ACL2 是基于[[BSD授权]]发布的[[开源软件]]。

== 简介 ==

ACL2 的编程语言可看作是一个[[函数式编程|函数式]]（无任何[[副作用]]）的 Common Lisp 变体。和 Lisp 一样，ACL2 使用动态类型系统。ACL2 中所有的[[子程序|函数]]均是完整定义的（{{link-en|Total functional programming|Total functional programming|total}}）——每一个函数均在 ACL2 的[[全集]]中将各个对象（输入）映射到另一个对象（输出）。

ACL2 的基础理论已将其程序语言的语义及其内置函数全部公理化。而程序语言中满足定义原则的用户自定义部分在扩展该理论的同时亦能保持其[[自洽|逻辑自洽性]]。ACL2 定理证明器的核心基于[[重写逻辑|项重写]]系统，此核心高度可扩展，用户已证得的定理可以在后续的[[猜想]]中被用作现成的[[数学证明]]。

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

2005年，Boyer-Moore 系列定理证明器（包括 ACL2）的开发者获得了[[ACM软件系统奖]]，获奖理由是“作为最高效的定理证明器的先驱和工程师……开发了能够用于验证硬件和软件可靠性的形式化工具”。<ref name=acmaward>{{cite web |publisher=[[计算机协会|ACM]] |url=http://awards.acm.org/homepage.cfm?srt=all&awd=149 |work=ACM Awards |title=Software System Award |accessdate={{date|2012|1|14}} |deadurl=yes |archiveurl=https://web.archive.org/web/20120402203501/http://awards.acm.org/homepage.cfm?srt=all&awd=149 |archivedate=2012-04-02 }}</ref>

== 应用 ==

ACL2 在若干领域得以应用<ref>{{Cite web |url=http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html |title=Books and Papers about ACL2 and Its Applications |accessdate=2014-01-24 |archive-date=2013-11-06 |archive-url=https://web.archive.org/web/20131106084302/http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html |dead-url=no }}</ref><ref>{{Cite web |url=http://www.cs.utexas.edu/users/moore/acl2/workshops.html |title=The ACL2 Workshop Series |accessdate=2014-01-24 |archive-date=2014-02-13 |archive-url=https://web.archive.org/web/20140213235252/http://www.cs.utexas.edu/users/moore/acl2/workshops.html |dead-url=no }}</ref>。
例如，在奔腾浮点除错误被曝光之后，斯特罗瑟·摩尔和马特·考夫曼运用 ACL2 证明了 [[AMD K5]] 处理器的浮点数除法运算的正确性。<ref>{{cite paper | id = {{citeseerx|10.1.1.43.3309}} | title = A mechanically checked proof of the correctness of the kernel of the AMD5K86 floating point division algorithm }}</ref> 在 ACL2 文档的有趣的应用<ref>[http://www.cs.utexas.edu/users/moore/acl2/v6-2/INTERESTING-APPLICATIONS.html 有趣的应用]{{Wayback|url=http://www.cs.utexas.edu/users/moore/acl2/v6-2/INTERESTING-APPLICATIONS.html |date=20131106084233 }}</ref>页面里有一些关于其实际应用的简介。

ACL2 的工业界用户包括[[超微半导体公司]]、[[Centaur科技]]、[[国际商业机器股份有限公司]]、[[英特尔]]、[[甲骨文公司]]和罗克韦尔柯林斯。

== 参考 ==

{{reflist}}

== 外部链接 ==

* [http://www.cs.utexas.edu/users/moore/acl2/ ACL2 website]*{{Wayback|url=http://www.cs.utexas.edu/users/moore/acl2/ |date=20120316201709 }}
* [http://acl2s.ccs.neu.edu/ ACL2s - ACL2 Sedan - An Eclipse-based interface developed by Peter Dillinger and Pete Manolios that includes powerful features to provide users with more automation and support for specifying conjectures and proving theorems with ACL2.]{{Wayback|url=http://acl2s.ccs.neu.edu/ |date=20101116150928 }}

{{程序设计语言}}
[[Category:LISP程式語言家族]]
[[Category:LISP程式語言]]
[[Category:程序设计语言]]

ACL2 - 版本历史

imported>HighSierra0820：​补充字词转换

imported>HighSierra0820：补充字词转换