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
.
- ^ 有趣的應用（頁面存檔備份，存於網際網路檔案館）
