| ACL2 | |
|---|---|
 | |
| パラダイム | 機能的、メタ |
| デザイン： | ロバート・S・ボイヤー、J・ストロザー・ムーア、マット・カウフマン |
| 開発者 | マット・カウフマンとJ・ストロザー・ムーア |
| 初登場 | 1990年[ 1 ]（限定配布）、1996年（一般配布） |
| 安定版リリース | 8.6 / 2024年10月 （2024年10月） |
| タイピングの規律 | 動的 |
| OS | クロスプラットフォーム |
| ライセンス | BSD |
| Webサイト | www |
| 影響を受けた | |
| Common Lisp、Nqthm | |
ACL2（A Computational Logic for Applicative Common Lisp）は、プログラミング言語、一階述語論理の拡張可能な理論、そして自動定理証明器から構成されるソフトウェアシステムです。ACL2は、主にソフトウェアおよびハードウェア検証のための、帰納的論理理論における自動推論をサポートするように設計されています。ACL2の入力言語と実装はCommon Lispで記述されています。ACL2は無料のオープンソースソフトウェアです。
概要
ACL2プログラミング言語は、 Common Lispの応用型（副作用のない）版です。ACL2は型付けされていません。すべてのACL2関数は、ACL2ユニバース 内の各オブジェクトを、同じユニバース内の別のオブジェクトにマッピングします。
ACL2の基本理論は、プログラミング言語と組み込み関数の意味論を公理化します。定義原理を満たすプログラミング言語におけるユーザー定義は、理論の論理的一貫性を維持しながら理論を拡張します。
ACL2 の定理証明器の中核は項の書き換えに基づいており、この中核は、ユーザーが発見した定理を後続の推測のアドホック証明手法として使用できるという点で拡張可能です。
ACL2は、ボイヤー・ムーア定理証明器NQTHMの「産業用」バージョンとなることを目指しています。この目標に向けて、ACL2は興味深い数学理論や計算理論のクリーンエンジニアリングを支援する多くの機能を備えています。また、ACL2はCommon Lispをベースに構築されていることからも効率性を得ています。例えば、帰納的検証の基盤となる仕様をそのままコンパイルし、ネイティブに実行することができます。
2005年、ACL2を含むBoyer-Mooreファミリーの証明器の作者は、「安全性が重要なハードウェアとソフトウェアを検証するための形式手法ツールとして、最も効果的な定理証明器の先駆的かつ設計的開発」に対してACMソフトウェアシステム賞を受賞した。 [ 2 ] [ 3 ]
証明
ACL2は数多くの産業用途に利用されてきた。[ 4 ] [ 5 ] 1995年、J Strother Moore、Matt Kaufmann 、Tom LynchはACL2を使用して、 Pentium FDIVのバグを受けてAMD K5マイクロプロセッサの浮動小数点除算演算の正当性を証明した。[ 6 ]
ACL2 の産業ユーザーには、AMD、Arm、Centaur Technology、IBM、Intel、Oracle、Collins Aerospace などがあります。
参照
参考文献
- ^ 「XDOC — Note-1-7」 . www.cs.utexas.edu .
- ^ 「ACM: プレスリリース、2006年3月15日」 。2008年8月1日。2008年8月1日時点のオリジナルよりアーカイブ。
- ^ 「Software System Award」 . ACM Awards . Association for Computing Machinery . 2012年4月2日時点のオリジナルよりアーカイブ。2012年1月14日閲覧。
- ^ 「ACL2注釈付き参考文献」www.cs.utexas.edu。
- ^ 「ACL2 ワークショップと UT ACL2 セミナー」www.cs.utexas.edu。
- ^ Moore, J. Strother; Lynch, Tom; Kaufmann, Matt (1996). 「AMD5K86浮動小数点除算アルゴリズムのカーネルの正確性に関する機械的検証による証明」IEEE Transactions on Computers . 47. CiteSeerX 10.1.1.43.3309 .
外部リンク
