bonotakeの日記

元・ソフトウェア工学系研究者、今・AI系エンジニア

スタートAlloyやりました

cf. http://atnd.org/events/27160

ジョーに適当な準備だけで(テキトーな資料でホントすいません)、しかも「習うより慣れろ」と吹いてAlloy言語のレクチャーほとんどなしに演習やってもらうという無謀な試みにも関わらず、(Alloy初心者の方々も含め)全体的に皆さん大健闘されまして、僕としてはうれしい誤算でした。

というか、やってみるもんだなぁ。僕もいろいろ勉強になりました。

当日の演習課題について

課題にしたのは「バージョン管理システムモデリング」。

  1. 1人だけで使う状況を考える
  2. 複数人で使う状況を考える
    • 1つのリポジトリを複数の開発者で共有する
      1. コンフリクトが起こる状況をモデル化する
      2. コンフリクト解消の機能をモデル化し、それで正しく動作することを確かめる
  3. 発展的課題

…と、3問用意していたのですが、実は1. だけでも半日〜数日は余裕で遊べる、ヒジョーに難しい課題でした*1

何が難しいかというとですね。
普通のOS上のファイルシステムなら、同一フォルダ内で同じファイルかどうか、というのは、同じファイル名かどうかで単純に区別がつきます。
ところが、バージョン管理システムでは、それ以外に

  • リポジトリ内とローカルファイルとで別々に存在するファイルが同一のものか否か
  • 同じリポジトリ内で、リビジョン違いの同一ファイルか否か

があり、「ファイル」という概念に3種類の同一性を導入しないといけないのです。

ということで、かなりハードだったはずです。でも皆さん、その全てではないにしても、問題の本質に気づいてそれなりにモデリングをこなされていたので、すばらしかったです。

AlloyモデリングのTips

で、今回皆さんのさまざまな反応を見て思った、Alloyでのモデリングのコツ。自分のためにも残しておきます。

とにかくシンプルに、シンプルに。

設計対象の本質(「抽象」)だけをモデル化していくべし。
言い換えると、「それがなかったら、このシステムは実現不可能」な概念だけを導入してください。
たとえば、バージョン管理システムに「ファイルの差分」という概念は、必ずしも必要ではないですよね。

自分の中の「仕様」を疑え。

プログラミングとAlloyを使ったモデリングは、似ているようで、決定的に違うところがあります。
それは、Alloyの出力結果が正しくて、自分の頭の中の仕様が間違ってるケースが多々あるということです。そもそも、元々ぼんやりとした要求しかないところから、仕様を考える作業をしているのだから、当たり前です。

だから、Alloyが変なインスタンスを出してきたからといって、すぐにバグ扱いしないでください。それ以前にまず、それをバグだとする判断が自分の思い込みではないのかを疑ってください。

想像力を働かせて、現実にそういう状況が起こりうるのか、起こっても大丈夫かが確認できたら、それはスルーして大丈夫なのです。むしろ積極的に、そういう状況を受け入れ可能なように、自分の脳内イメージを改めてください。

制約を緩めることも大事。

上記を踏まえた上で)どう考えてもあってはならないインスタンスが出力されたら、それはモデルに制約を追加するときです。
一方、意図したようなインスタンスが出力されなかったら、それは十中八九モデル中の制約が強すぎるときです。なので、このときは逆に、制約を緩めないといけません。ここで更に制約を追加すると、おかしなことになります。

そして、注意すべきは、制約が少なければ少ないほど、システムは堅牢になるということです。制約とはシステムが正常動作する前提条件です。余計な前提条件があればあるほど、脆いシステムになってしまいます。

*1:実際のところ、難しすぎるなーと思って予備に回していたお題だったのですが、本命で考えていた課題が、自分でやってみると逆に単純すぎて、直前で取りやめざるを得なかったのでした。

注:bonotakeは、amazon.co.jpを宣伝しリンクすることによってサイトが紹介料を獲得できる手段を提供することを目的に設定されたアフィリエイト宣伝プログラムである、 Amazonアソシエイト・プログラムの参加者です。