『抽象によるソフトウェア設計』とAlloyã€ç¬¬ä¸€å°è±¡å ±å‘Š

『抽象によるソフトウェア設計 -- Alloyではじめる形式手法』の献本をいただきました*1。書店に並ぶ前、7月9日に届きました。訳者のみなさん、ありがとうございます。

抽象によるソフトウェア設計−Alloyではじめる形式手法−

「序文」、「監訳者序文」、「訳者あとがき」、そして第1章「はじめに」あたりを読んで感心しておりました。第1章はわずか4ページですが、素晴らしい、実にいいことが書いてあります。それで僕はスッカリ満足して（残りは読まないままで ^^;）いました。

金曜日（7月15日）にid:bonotakさんに、「アンタ、いくらなんでも2章くらいは読んでミソ」とメールで言われまして、第2章「ざっと一巡り」を読み始めたんですが、こういうクイックツアーみたいなのは、僕、苦手なんですよ。

第2章の冒頭に「手法の雰囲気を伝えることが目的なので、細部まで理解しようとはしないでほしい。」と。細部に入る前に、全体像を概括的に捉えておくことは有意義だし、僕もたまにそんな目的の記事を書いたりもするんですが、サンプルコード断片の構文とかが気になって、概要を把握するよりフラストレーションがたまってしまったり…。それでどうしたか、って話は後回しにして、書籍の印象を書いておきます。今でも読んでない所のほうが多いので、評価じゃなくてあくまで印象。

1. 紙の本は、モノとしての形態がすごく気になるのですが（e.g. 「ハードカバー本なんて大嫌いだ」、「清水明著『量子論の基礎』はいい本だ」）、その点では使い勝手がいいです。
2. 付録が便利でとても助かります（つーか、主に付録を読んでるんですが）。
3. 訳語一覧があるのも好感が持てます。欲をいえば、もう少し語数が多いと良かったかな。例えば、「基本型」は訳語一覧には載ってません； 「基本」と訳す言葉に base, basic, primitive, atomic, ground, fundamental とかありますからね、モトを知りたい。
4. 一区切り付くごとに「議論」の項がはさんであります。「議論」は設計者本人でないと語れない内容、とても面白く有意義です。

僕がしたこと

とりあえずAlloyの言語仕様を把握しようと、付録B「Alloy言語リファレンス」を読むことにしたのですが、けっこう長い。で、付録C「中核の意味論」なら短い（2.5ページ）ので、こっちを読破（2.5ページだって）。意味論がわかった気分がしたので、http://alloy.mit.edu/alloy4/ から alloy4.jar をダウンロードしました。

[追記]僕は、最初バージョン4.1.10をダウンロードしたのですが、bonotakeさんによると、4.2 Release Candidateのほうがオススメだそうです。[/追記]

java -jar alloy4.jar とすると、メニューが付いたウィンドウが出てきて、ここで少しゲンナリ。僕、GUIは苦手。コマンドラインインターフェイスがないと使う気がしない。ところが、18日の昼くらいから、bonotakeさんがGUIの操作法やらコツやらをメールで教えてくれたので、ナントカかんとかAlloyアナライザーを使える（？）ようになりました。

bonotakeさんに教わったことをまとめておくと：

1. 外部エディタでソースコードを編集した場合は、CTRL-Rでリロード。
2. ビジュアライザーのEvaluatorボタンでインタプリタが出てくるので、これを使ってモデルインスタンスをインスペクトできる。
3. ビジュアライザーのNextボタンを押すと、別解を次々に表示できる。

あと、OptionsメニューのMessage Verbosityをhighに、Visualize AutomaticallyをYesに設定しておくと良いようです。

Alloy処理系自体のソースコードはalloy4.jarに含まれるので、次のようにしておくとソースを参照できます。

$ mkdir src

$ cd src

$ jar xvf ../alloy4.jar

$ find . -name '*.class' | xargs rm

./src/edu/mit/csail/sdg/ の下にAlloy4関係のソースが展開されます。Javadocは、http://alloy.mit.edu/alloy4/public/ で閲覧できます（これもbonotakeさんに教わりました）。

あとは、『抽象によるソフトウェア設計』（Alloy本）の付録Bと付録Fを適宜参照すれば、Alloyでモデリングをはじめられるでしょう。

Alloy言語でなんか書いてみた

次は、僕がはじめて書いたAlloy言語による仕様記述です。

-- モノイド
module monoid1 


/* モノイドの指標 */

sig Mon {
 -- 乗法
 mult : Mon->one Mon
}

one sig pt {
 -- 単位
 unit : Mon
}

/* モノイドの公理 */

-- 結合律
fact assoc {
 all x, y, z : Mon | 
   (x.mult[y]).mult[z] = x.mult[y.mult[z]]
}

-- 単位律
fact unit {
 all x : Mon |
   pt.unit.mult[x] = x 
   and 
   x.mult[pt.unit] = x
}

とりあえず思いついた例がモノイドだったので、モノイドの定義をそのままAlloyに直訳。でも、sig Mon {...} のように余代数形式で書かなくてはならないので、モノイドの乗法 Mon×Mon→Mon を、this |→(Mon→Mon) のような形で書く必要があります。

普通の（手書きの）書き方に近づけたいなら、モノイドの乗法も単位もグローバルに定義する書き方もできます。ここで、グローバルと言っているのは、一点集合pt（pointのつもり）のことで、乗法と単位をptのシグネチャとして書くわけです。“一部”の人が大好きな、大域関数に相当するスタティックメソッドと幾分似てなくもないです。

-- モノイド その2: 単位も乗法もグローバルに定義してみる
module monoid2 


/* モノイドの指標 */

-- 単なる集合
sig Mon {}

-- 単位と乗法はグローバルに
one sig pt {
 -- 単位
 unit : Mon,
 -- 乗法
 mult : Mon-> (Mon-> one Mon)
}

/*モノイドの公理 */

-- 結合律
fact assoc {
 all x, y, z : Mon |
   pt.mult[pt.mult[x, y], z] = pt.mult[x, pt.mult[y, z]]
}

-- 単位律
fact unit {
 all x : Mon |
   pt.mult[pt.unit, x] = x 
   and 
   pt.mult[x, pt.unit] = x
}

以上のような仕様を、Alloyビジュアライザーで眺めてみると、こういう書き方はどうもAlloyに慣れてない人がやることみたいですね。グローバルを表現する一点集合を導入するより、モノイドの台集合Monの部分集合*2として単位元を導入したほうが良さそうです。

-- モノイド その3: 単位にサブタイプを使う
module monoid3


/* モノイドの指標 */

sig Mon {
 -- 乗法
 mult : Mon->one Mon
}

-- 単位元（単元の部分集合）
one sig unit extends Mon {}

/* モノイドの公理 */

-- 結合律
fact assoc {
 all x, y, z : Mon | 
   (x.mult[y]).mult[z] = x.mult[y.mult[z]]
}

-- 単位律
fact unit {
 all x : Mon |
   unit.mult[x] = x 
   and 
   x.mult[unit] = x
}

ビジュアライズしてみる

Alloyアナライザーが探しだした仕様のモデルインスタンスは、Alloyビジュアライザーで自動的に絵に描くことができます。この絵は万能というわけではなくて、前節のモノイドのごとき代数構造だと、よくワカンナイ絵になりがちです。ですが、状態遷移の記述は、Alloyビジュアライザーとの相性がバッチリで、自然で分かりやすい絵を描いてくれます。

次はスタックの記述です。

-- スタック その2: 空状態、フル状態をサブタイプに
module stack2

-- スタックに積む値
sig Val {}

-- スタックの状態と操作
sig State {
 push: Val ->lone State,
 pop: lone State,
 top: lone Val
}

-- スタックが空の状態
one sig empty extends State {}

-- スタックがフルの状態
one sig full extends State {}

/* スタックに関する公理 */

-- スタックトップ値の取得
fact top {
 all s: State |
   (s != empty => one s.top)
   and
   (s  = empty => no s.top)
 }

-- ポップした後の状態
fact pop {
 all s: State |
   (s != empty => (one s.pop) and s.pop != s)
   and
   (s  = empty => no s.pop)
}

-- プッシュした後の状態
fact push {
 all s: State, v: Val |
   (s != full => one s.push[v] and s.push[v] != s)
   and
   (s  = full => no s.push[v])
}

-- プッシュした後のトップの値
fact push_top {
 all s: State, v: Val |
   s != full => s.push[v].top = v
} 

-- プッシュの後にポップすると
fact push_pop {
 all s: State, v: Val |
   s != full => (s.push[v]).pop = s
}

-- ポップを繰り返すと空になる
-- これがないと絵に不連結グラフが出てくる
fact pop_reachable {
  all x: State |
   x != full => x in full.^pop
}

ビジュアライザーによる表示（の一例）は次のようになります。

Stateと書いてある箱は、状態空間全体のことではなくて、emptyでもfullでもない第三の状態のことです*3。要するに、スタック上に値が0個（empty）、1個（State）、2個（full）という状態がある、ってことです。

赤い矢印がpop（スタックのポップ）による状態遷移で、「full状態→値が1個の状態→empty状態」と遷移しています。薄茶色の矢印はpush（スタックのプッシュ）による状態遷移で、popと逆の経路になっています。オレンジは、スタックトップ値を返す関数で、状態空間の各状態（合計で3つの状態）から値の集合Valへの矢印ですね。矢印が状態遷移か関数かなんてことはAlloy処理系は知りませんが、我々がそういう解釈を与えるのです。

[追記] スタックの制約（fact）で、(s != empty => one s.top) and (s = empty => no s.top) って書いてありますが、これは、s != empty implies one s.top else no s.top または、s = empty implies no s.top else one s.top とより簡潔に書けるようです。一般に：

• (A => X) and (!A => Y) ≡ A implies X else Y ≡ A => X else Y

fact pop_reachable は、コメントと内容がずれてました。コメントのとおりに制約を書くなら x != empty => empty in x.^pop ですね。[/追記]

[さらに追記]推移的閉包演算子「^」だけじゃなくて、反射的推移的閉包演算子「*」もあるんですね。「*」を使えば、fact pop_reachableの x != empty という前提をチェックする必要はなくて、一律に empty in x.*pop と書けます。「*」には反射的閉包も入るので、empty in empty は自明に成立します。組み込み演算子を使うことが短く書くコツみたい。[/さらに追記]

これは面白い！

半日ほどですが、僕はサルになってAlloyアナライザーをズーッといじってました。とにかく面白い。その感想を書いてbonotakeさんに送ったメールの一部をそのまま引用します。

2011年7月18日16:58 Masayuki Hiyama :

>> 変な状態遷移図を探してくるので面白い。

>

> いやー、おもろいなー、コレー。

>

> 最近、子供の相手しないから、休日の遊びがAlloyになってしまった。

>

> どこが面白いか？というと、人間が一人（自分だけ）でもコンピュータ相手に

> “エクソシストゲーム”ができる。

>

> - http://d.hatena.ne.jp/m-hiyama/20060407/1144378577

> - http://d.hatena.ne.jp/m-hiyama/20060408/1144479281

>

> 律儀に悪魔の役をやってくれる人間なんていないけど、Alloyアナライザーが悪

> 魔のターンを実行してくれるので、俺のターンでは仕様を詳細化してだんだん

> 追い詰める。インスタンスが一意になるほど追い込む必要はないけど、奇妙な

> 事例が出ない程度まではターンを続けないとね。

>

> 僕にとっては、これは完全に娯楽ソフトウェアだな。

>

実を言うと、ひととおり出来上がったAlloyコードを示しても楽しさは伝わらないと思います。ゲームのように楽しめるのは、未完成なコードをAlloyアナライザーに解析（モデルインスタンスの検索）させているときです。思いもかけない奇妙な例を探し出してきます。苦笑したり、ビックリしたり、ゲラゲラ笑ったり。そのプロセスが面白いのです。まさに、「俺のターン」「おまえのターン」を繰り返すセッションです。

自分で定義して創造したはずの抽象的構造物たちの空間内に、自分の予想を裏切る変なヤツが生息していることを実感できます。この感覚を味わうだけでもAlloyアナライザーを使ってみる価値はあると思います。そして、書籍『抽象によるソフトウェア設計 -- Alloyではじめる形式手法』は、その探検への最良のガイドブックであり、またそれ以上のものです。

*1:僕は何の貢献もしてません、恐縮です。

*2:正確に言うと、シグネチャMonの意味である集合の（単元な）部分集合です。

*3:箱にState$0のようなラベルを付けるほうがいいと思いますね。