Alloy とかいう形式仕様記述言語があります。ソフトウェアの仕様を形式的に記述して検証とかして、上流設計をうまいことこなしちゃおう、とかいうアレです。
で、Alloy の教科書とされる「Software Abstractions: Logic, Language, and Analysis」という本があります。
The MIT Press
売り上げランキング: 28680
↑ここぞとばかりにアフィリエイト入ってみた。みんな絶対買うなよ！
で、最近この本の翻訳に関わってました。bonotake さんや masahiro_sakai さんのお手伝い的な感じに。
で、そろそろ翻訳の目処がたってきたので、レビュワー募集の告知のためにこの記事を書いてます。
- 募集人員：若干名
- 期間：3月初旬から3月いっぱいまで（予定）
- 応募方法： takeo.bono at gmail.com にメール または twitterで @bonotake にmentionしてください。
手を挙げていただいた方のうち何名かを選抜して、2/22以降にこちらから声をかけさせていただきます。（応募頂いても、残念ながらお願いしない場合がありますので、悪しからずご了承下さい）
Alloyの知識あるなしは問いません。ユーザー、あるいは入門者の視点で読んでくださる方歓迎です。
興味のある方はどうぞよろしく。
Alloy は基本的にはソフトウェア開発の上流設計で使うものなんですが、パズルの探索なんかにも使えます。問題の定義を書くだけで、解答を見つけてくれる感じです。
簡単な例として、Alloy でナイト・ツアーを形式化してみました。「チェスのナイトをチェス盤の 64 マスすべてに 1 回ずつ訪問させよ」というパズルです。
-- 各状態は順序付けされている
open util/ordering[State] as states
-- 各状態ではナイトがどこかのマスにいる (今ナイトがいるマスを表す整数 x と y を持つ)
sig State { x, y: Int }
-- 述語 knight: 状態 s と t がナイトの移動 (桂馬飛び) になっている
pred knight[s, t: State] {
(dist1[s.x, t.x] and dist2[s.y, t.y]) or (dist2[s.x, t.x] and dist1[s.y, t.y])
}
-- 補助述語: 整数 i と j の差が 1 (または 2) である
pred dist1[i, j: Int] { (i < 3 and i + 1 = j) or (j < 3 and j + 1 = i) }
pred dist2[i, j: Int] { (i < 2 and i + 2 = j) or (j < 2 and j + 2 = i) }
-- 述語 solve: クリア条件
pred solve {
-- 同じマスを通らない (異なる状態でナイトが同じマスにいることはない)
all disj s, t: State | s.x != t.x or s.y != t.y
-- 盤面すべてのマスを網羅している
-- (上の条件だけで十分だが、これも書いた方が探索空間が減るはず)
Int -> Int in ~x.y
-- 連続する状態はすべてナイトの移動になっている
all s: State | s != last => knight[s, next[s]]
}
-- 状態数は 64 (8x8 = 64 マスなので) 、整数は 3 ビットで表現される
run solve for exactly 64 State, 3 int↑Alloy の色付けができないなんて、はてなめ……。Alloy 知らなくてもなんとなくわかるところもあると思います。わからないところもあると思いますが、詳しいことは本を読んでください :-)
これを Alloy にかけると以下の答えがでてきます *1 。まあパズルとかは Alloy のメインターゲットでないので、答えを見つけるまでに 1 時間半くらいかかりましたが、そこは愛嬌。
44 41 30 51 06 03 32 01 29 50 45 42 31 18 61 04 40 43 28 07 52 05 02 33 49 08 39 46 17 60 19 62 12 27 48 53 38 23 34 59 09 54 11 16 47 20 63 22 26 13 56 37 24 15 58 35 55 10 25 14 57 36 21 64
