Hatena::ブログ(Diary)

まめめも このページをアンテナに追加 RSSフィード

2011-07-08

[] 「抽象によるソフトウェア設計」が発売されます

来週には RubyKaigi ですが、Ruby とは全く関係ない話題。

半年前にレビュワーを募集していた Software Abstraction 翻訳本ですが、とうとう発売されることになりました。今月中旬には書店に入るはずで、今日私の手元にも見本が届いたところです。みんな各自 100 冊くらい買ってください。


抽象によるソフトウェア設計−Alloyではじめる形式手法−
Daniel Jackson
オーム社
売り上げランキング: 35132

アフィリエイト注意。みんな絶対クリックするなよ!


Alloy とかいう形式手法の教科書です。Alloyソフトウェアの仕様を形式的に記述して検証とかして、上流設計をうまいことこなしてください。

有界モデル検査とか言うと敷居が高く聞こえるかもしれませんが、比較的こむずかしいこと考えなくてもモデル化できるし、比較的大きな問題でも解けるかもしれません。

モデル化の言語の「すべての値は関係である」「操作は関係演算 (SQL の join とかみたいなの) で表現する」というあたりは、ある意味 esoteric language みたいな面白さがあります。(とかいうと普通の人は引きそうだけど、もちろん普通にも使える)


そういうわけで、是非買ってください。宣伝でした。


訳者:

編集さん:

サポートページ

2011-02-08

[] Software Abstraction 翻訳本のレビュワー募集

Alloy とかいう形式仕様記述言語があります。ソフトウェアの仕様を形式的に記述して検証とかして、上流設計をうまいことこなしちゃおう、とかいうアレです。

で、Alloy の教科書とされる「Software Abstractions: Logic, Language, and Analysis」という本があります。

Software Abstractions: Logic, Language, and Analysis
Daniel Jackson
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

*1:実際には x や y への変数割り当てが xml 表記で手に入るだけなので、そこから軌跡に変換する必要はあります。