ACL2を触ってみる

最近形式検証に興味があるので、ACL2を触ってみた。

形式検証とは

仕様を特定の形式で書くと正しさをチェックしてくれる、らしい。

ALC2とは

Common Lispで書かれた形式検証のツール。

• ACL2 Version 8.3
• GitHub - acl2/acl2: ACL2 System and Books as Maintained by the Community

環境

uname -a
Linux gx502g 5.4.0-77-generic #86-Ubuntu SMP Thu Jun 17 02:35:03 UTC 2021 x86_64 x86_64 x86_64 GNU/Linux

ros --version
roswell 21.06.14.110(c0bc597)

ros run -- --version
SBCL 2.1.6

インストール

asdはなさそうでmakeする必要がある。

ACL2 Version 8.3 Installation Guide

ダウンロードして展開する。

wget https://github.com/acl2/acl2/archive/refs/tags/8.3.tar.gz
tar xf 8.3.tar.gz

ビルドして.localに実行ファイルをコピーする。

cd acl2-8.3/
make LISP="ros run"
cp saved_acl2 $HOME/.local/bin

手順にしたがってbooksをビルドする。

cd books
make -j 16 ACL2=$HOME/.local/bin/saved_acl2 basic

チュートリアル

チュートリアルの A Walking Tour of ACL2 をやってみる。

saved_acl2

で起動して、説明読みつつ実行してみるが、これ自動定理証明系か。 これ自体はよいものかもしれんが、俺が今欲しかったのはこういうのじゃなかった。。。