B Methodを試してみた
本を読んである程度勉強したので、実際に試してみることにしました。
B4Freeというツールが無料で使えるようなので、試してみることに。
Webサイトがフランス語で面食らいましたが、
右上のイギリス国旗の画像を押すと英語で読めます。
しかし、DownloadページにLinux版はあるもののFreeBSD版が存在しませんでした。
まあ、きっと大丈夫だろと信じてLinux版をダウンロード。
そして、B4Freeインストールの手引きに従い無事インストールを済ますことができました。
Click’n’Proveというツールを入れると、対話的に証明が出来るらしいのですが、
使い方がよく分かりませんでした。なんてこったい。
演算子を入力すると対応する数学記号になって表示されるのは面白かったのですが、
Bのソースを元にCのコードを生成する方法がなさそうだったので、
コマンドライン上で動作するbbatchを使って開発をしてみることに。
資料が見当たらなかったのでヘルプを見ながら直感に頼って試してみました。
なにかおかしなことやってたら誰か教えて。
$ cd ~/B4Free-3.2 $ mkdir switch $ cd switch $ mkdir pdb # プロジェクトのデータを格納 $ mkdir lang # トランスレートにより生成されるファイルを格納 $ mkdir src $ cd src $ vi switch1.mch # 内容はCommenCのサンプルを参照 $ vi switch1_i.imp # 内容はCommenCのサンプルを参照 $ cd ~/B4Free-3.2 $ ./bbatch -r=./B4free.rc Beginning interpretation ... bbatch> crp switch switch/pdb switch/lang # プロジェクトの作成 bbatch> op switch # プロジェクトを開く bbatch> af switch/src/switch1.mch # ファイル(Abstract Machine)の追加 bbatch> af switch/src/switch1_i.imp # ファイル(Implementation)の追加 bbatch> t switch1 # 型チェック bbatch> pr switch1 0 # 自動証明 bbatch> t switch1_i # 型チェック bbatch> pr switch1_i # 自動証明 bbatch> b2c switch1_i # Cへトランスレート
ちゃんとCのソースが生成されました。やったね。
今度は自分でプログラム(というより仕様)を書いてコード生成をしてみようと思ったのですが、
簡単なものは作れたものの、少し複雑なものを作ろうとすると、
自動証明では証明できないものが生まれてきて、詰まってしまいました。
対話的な証明を行う方法がよくわからないうえに、対話的でない証明をする方法も分からず。
ASSERTIONS節に適切な表明を書けばほとんど自動証明だけで済むらしいのですが、
結局証明できない箇所(しかもそれが何処か分からない)が残ってしまい断念。
それはさておき、今週もCLANNAD ASは凄くよかったです。
美佐枝さんシナリオはやっぱり重要ですよね。
来週はゆきねぇシナリオのようでこちらも期待。
まあ、それも置いといて、いつしかのリリカルの続き。
