Alloyを理屈っぽく考えてみようと思う

Alloy本＝『抽象によるソフトウェア設計』が出版された直後、しばらく僕はAlloyで遊んでました。「『抽象によるソフトウェア設計』とAlloy、第一印象報告」あたりからいくつかAlloy関係の記事を書いています。でも、2,3週間で「ちょっと飽きたかなー」と。サンプルの人生モデリングも途中までで、続編は西尾さんにお任せ（「お願いした続編です： Alloyで人生モデリング」）。

このとき僕は、Alloy本をソフトウェアのマニュアルとして読んでいて、Alloyアナライザーを使うために必要な箇所を拾い読みしただけです（著者、翻訳者の皆さん、ゴメンナサイ）。最近になって、頭から（でも第2章はスキップ）読んでます。Alloyアナライザーの背後にある理屈のほうを読み取ろうと思っています。

キッカケはスピヴァックの関手データモデルです。「デイヴィッド・スピヴァックはデータベース界の革命児か -- 関手的データモデル」のコメント欄でid:bonotakeさんとのやり取り（http://d.hatena.ne.jp/m-hiyama/20130128#c1359936671 ）で、

AlloyモデルとRDBが似てる、とかじゃなくて、まったく同じ概念を具現化しているとなれば、Alloyでデータベース設計やプロトタイピングがすごく実際的になる気がします。

関手データモデルとAlloyは、かなり親和性が高いんじゃないか、と感じるのです。以前から、Alloyを圏論的に解釈できないか？とは考えていて、「Alloyの矢印記法と、モノイド閉圏としての関係圏」、「Alloy、コンパクト論理、関係圏」なんて話も書きました。また、関手データモデルを理解する道具としてAlloyが役に立つとも言えます。

と、そんな事情で、Alloy本＝『抽象によるソフトウェア設計』を読み直しながら、Alloyを理屈っぽく考えてみようと思っている次第です。

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