「抽象によるソフトウェア設計」発売
https://sites.google.com/site/softwareabstractionsja/
https://sites.google.com/site/softwareabstractionsja/about/toc ← 目次
本日7月15日金曜日、洋書「Software Abstractions」(http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=10928)の訳本である「抽象によるソフトウェア設計 Alloyではじめる形式手法」が発売されます。
実はレビュワーだったりしたので、発売当日になってしまいましたが、勝手に紹介するつもりです。
さて、本書はサブタイトルの通りでAlloyを使って何か色々しましょうという感じになっています。
いや、そもそも"Alloy"って何やねんという話なのですが、Alloy 知らなくても読めるという感じのするサブタイトルですね！！
(ちなみにAlloyの最新バージョンであるAlloy4は次のサイトから入手出来ます → http://alloy.mit.edu/alloy4/)
中身の紹介に入る前ですが、皆さん、「抽象」「設計」「はじめる〜」「形式手法」などの文字列が目に入り込んで来た瞬間に「はぁまたこのような本が出たとは！」「読んでも何も変わるまい」「まぁわたくしには関係ありませんわね(迫真)」などなど考えた筈です。
宣伝にあたってこう書くとなんですが、本書は「はじめる形式手法」とかゆるふわっぽいタイトルになっているものの、実はそんなに簡単な内容ではないという所が味噌です。かなり骨のある書だと思います。
うだうだ言っても何なので、そもそもAlloyで何が出来るのか。
そんな上手く短く書けないので、インターネット上に存在するAlloyの良いtutorialへのリンクを貼ってみます。
http://people.csail.mit.edu/eskang/talks/alloy-tutorial-abz2010.pdf
Alloyは非常に簡単に言うと「関係論理」という論理の1種を用いて、調べたい対象を記述、それと同時に対象において成立するべき/成立してはならない事柄を書いて、それが正しくそうなっているかどうかを調べるというものです。
「正しくそうなっている」かどうか、どうやって確認するのか? というのは、何それの事柄を満たす「モデル、インスタンス、具体例」を発見出来るか、発見出来ないかによって調べるのです。
モデルを発見しようとするのがAlloyの仕事です。あることを証明したり、ないことを証明したりするわけではありません。
関係論理って何やねんという話ですが、関係(relation)を要とする論理系の一種とかその程度の理解で十分です。
さて、このAlloyを使ってどのような対象にあれやこれやを記述する事が出来るのでしょうか?
例えば、上述のtutorialの最初の方では「アドレス帳」を書いています。
sig Name , Addr {}
sig Book {
addr : Name -> lone Addr
// お手軽にloneて何なのか知りたい そこのあなたは、是非本で確認してください
}Nameというモノ(名前を意図しています)の集まり、Addrというモノ(アドレスを意図しています)の集まりを1行目で定義しているのです。
3行目からは、Bookというモノ(意味的にはアドレス帳)と、addrという「関係」を定義しています。
この関数っぽく見える関係addrですが、(アドレス帳 , 名前 , アドレス)の3つ組に関する関係になっています。
このような関係を定義して、その上で色々やるというのがAlloy上で行う事になるのですが、果たしてどんなものなら記述出来るのでしょうか?
例えば、固定したアドレス帳のある瞬間における静的な状態として、1つの名前に対して登録出来るアドレスは「高々1件である」という制約(上述のAlloyコードはそういう事を述べている)は記述出来るわけですが、では動的な操作に対してはどのようにすれば良いでしょう。
えーと…アドレス帳上では追加や削除といった操作を行ったりします。
ここで追加や削除は実装されているとして、実装はさておきで追加や削除が「満たすべき」振舞というものは存在します。
アドレス帳に存在しない名前に対してアドレスを登録した(追加)。 そしてその直後にその名前を消した(削除)ならば、元のアドレス帳と同じになっていなければならない。
そのような追加と削除に関する簡単な仕様は記述出来ます。
この手の「シミュレーション」ぽい事をどう行うのかというのはイディオムとしても、設計を行う上でも大変重要なものです。先のtutorialではざっくり様々な方法を書いていますが、詳しくは本書を手に入れてくださいという事で…。
Alloy何が面白いの?
何ソレが出来るみたいなポジショントーク的なものはさておき、Alloyを使っていて面白いのは自分が直面している問題をどうAlloyで取り組める/取り組み易い形にエンコードするかという事です。
Alloyは実際書いてみると分かりますが、(ほぼ)1階述語論理を使って様々なものを捉え直す必要が出てくるわけで、状態を激しく持ち回すようなものや、実際に実装しなければならないフルセットでエンコードするとか、そういったものは上手くいかないだとか、面倒臭いという事が多いものです。
結果的に取捨選択のもとでエンコードする事が多く成るわけですが、それは問題を抽象化してシンプルにするという事だけでは足りず、問題の捉え直しが必要だったり、一般化が必要になったりします。
ある種の縛りプレイのようなものだと思うのですが、それによって結果的に見通しや理解が深まる事というのは意外にも多いです。というより単純に楽しいです。
そして、このような論理を用いた「あれこれ」の記述に、慣れる事が出来るというのも大切なことだと思います。
巷では定理証明支援系が云々というのがありますが、何にせよ「自分の言いたい事をどう形式的に記述するか」という能力は問われるものです。そのような能力を養う事も出来ると思います。
この「Alloyでどう書く?」的な具体例の1つとして、tutorialの最後の方で出てくる「Checking Data Refinement」が面白いと思います。
