cf. http://atnd.org/events/27160
ヒジョーに適当な準備だけで（テキトーな資料でホントすいません）、しかも「習うより慣れろ」と吹いてAlloy言語のレクチャーほとんどなしに演習やってもらうという無謀な試みにも関わらず、（Alloy初心者の方々も含め）全体的に皆さん大健闘されまして、僕としてはうれしい誤算でした。
というか、やってみるもんだなぁ。僕もいろいろ勉強になりました。
当日の演習課題について
課題にしたのは「バージョン管理システムのモデリング」。
- 1人だけで使う状況を考える
- 複数人で使う状況を考える
- 1つのリポジトリを複数の開発者で共有する
- コンフリクトが起こる状況をモデル化する
- コンフリクト解消の機能をモデル化し、それで正しく動作することを確かめる
- 発展的課題
- 既存のバージョン管理システムが持つ他の機能をモデル化する
- ブランチ作成、マージ
- リポジトリが複数ある状況（分散バージョン管理）
- 既存のバージョン管理システムの気になるところを検証してみる
- 最強のオレオレバージョン管理ツールを考える（自由課題）
…と、3問用意していたのですが、実は1. だけでも半日〜数日は余裕で遊べる、ヒジョーに難しい課題でした*1。
何が難しいかというとですね。
普通のOS上のファイルシステムなら、同一フォルダ内で同じファイルかどうか、というのは、同じファイル名かどうかで単純に区別がつきます。
ところが、バージョン管理システムでは、それ以外に
があり、「ファイル」という概念に3種類の同一性を導入しないといけないのです。
ということで、かなりハードだったはずです。でも皆さん、その全てではないにしても、問題の本質に気づいてそれなりにモデリングをこなされていたので、すばらしかったです。
AlloyモデリングのTips
で、今回皆さんのさまざまな反応を見て思った、Alloyでのモデリングのコツ。自分のためにも残しておきます。
とにかくシンプルに、シンプルに。
設計対象の本質（「抽象」）だけをモデル化していくべし。
言い換えると、「それがなかったら、このシステムは実現不可能」な概念だけを導入してください。
たとえば、バージョン管理システムに「ファイルの差分」という概念は、必ずしも必要ではないですよね。
自分の中の「仕様」を疑え。
プログラミングとAlloyを使ったモデリングは、似ているようで、決定的に違うところがあります。
それは、Alloyの出力結果が正しくて、自分の頭の中の仕様が間違ってるケースが多々あるということです。そもそも、元々ぼんやりとした要求しかないところから、仕様を考える作業をしているのだから、当たり前です。
だから、Alloyが変なインスタンスを出してきたからといって、すぐにバグ扱いしないでください。それ以前にまず、それをバグだとする判断が自分の思い込みではないのかを疑ってください。
想像力を働かせて、現実にそういう状況が起こりうるのか、起こっても大丈夫かが確認できたら、それはスルーして大丈夫なのです。むしろ積極的に、そういう状況を受け入れ可能なように、自分の脳内イメージを改めてください。
*1:実際のところ、難しすぎるなーと思って予備に回していたお題だったのですが、本命で考えていた課題が、自分でやってみると逆に単純すぎて、直前で取りやめざるを得なかったのでした。
