Alloyで僕が最初に書いてみたのはモノイドの定義です。
群、環、体のようなお決まりの代数構造も、定義を直訳すればAlloyモデルを書けます。台集合が（比較的小さな）有限集合である構造を列挙したり調べたりできます。
ただ、代数構造だと、Alloyビジュアラザーの表示では辛いですね。解のデータを後処理して別なフォーマットにしないとよくわかりません。後処理の例は、エイトクイーン問題でやってみました。
ですが、ここで試した方法は行き当たりばったりなやり方なので、もっと系統的な手法と道具が欲しいところです。
順序構造やグラフなどは、Alloyと相性がよくて、定義も表示も割と自然にできます。
と、そんなわけで、なんらかの有限構造の例や反例を探し出す目的で、Alloyはかなり汎用的に使えます。が、Alloyの本来の／本命の用途はソフトウェアの抽象モデリングです。ソフトウェアでは、時間が絡んでくることが多いので、Alloyで時間概念の扱いの練習をしたいな、と思いました。
例題は何がいいか？ 思いついたのは人生のモデリングです。とはいってもたいしたことじゃないですよ。生まれて結婚して子どもができて死んでいく、という極めて基本的なエポックだけを扱います。
そんなに複雑にはならないでしょうが、それでも一度に書くのは大変なんで何回かに分けてダラダラいきます。予定はあんまりハッキリしないけど、3,4回かな？
「『抽象によるソフトウェア設計』とAlloy、第一印象報告」にも書いたように、Alloyでは出来上がったモデル記述よりは、それに至る過程が面白くもあり重要だと思うのです。アナライザー／ビジュアラザーと対話しながら、「あーでもない、こーでもない」と考えたり実験したりしながらモデル記述をしていきます。試行錯誤、紆余曲折がものすごく安いコストで実行できるのがAlloyのいいところでしょう。だから、少しずつダラダラふらりふらりはAlloyっぽいとも言えるでしょう、たぶん。
さてここで、モデルの前提に関して、いくつかの政治的弁明をしておきます。まず、人（human）を男と女に分けます。これは排他的和集合になります。それでいいのか？ とも考えたのですが、出生届の段階で性別は記入するので、人は男女どちらかに確定することを前提とします。その他、日本の現状の制度にだいたいは従うようにしています。同性結婚、一夫多妻、一妻多夫は認められてないので、婚姻は「男1、女1」の多重度の関係だとします。
こんな前提で、これ以上は現実世界の諸問題とは関わらずに、抽象的なモデリングをしたいと思います、ダラダラと。
