Tutorial for Alloy Analyzer 4.0

和訳というほどではないですが，簡単にまとめます．元の Tutorial はこちら．
いろいろ端折ったり意訳したりしてるので，参考程度で～．

Chapter. 0

間違ったサンプルモデルを正していく流れでチュートリアルを行う．
一般的なモデリングっぽいだけでなくて，単純な構文からなるモデルから初めてどんどん難しい文法や複雑なモデルを使っていくことで理解できるようになっているらしい．もちろんすべての文法を使うわけではない．

例えば社内で郵便物を転送する場合，1. 転送の手続きを決め，2. 配達方法に何らかの制約を設け，3. 正しく配達されるかどうかを確かめる，という手段をとる．
それと同じで，

というのがモデルを記述することのゴールである．

Alloy を使うことで，「この性質はサイズが $X$ までのモデルで成り立つ」とか「この性質はいつでも成り立つわけではなくて，その反例がこれ」ということを提示してもらえる．

モデリングでは以下の問題が起こる：

モデル自身に含まれる誤り：
条件が多すぎるとか少なすぎるとか．なくしたいやつ．多分モデルの書き方が悪いとか，意図していない制約を書いちゃってるとか，そういうやつ．
モデリングしている対象の誤り：
モデリングしている対象の内容が誤っているかどうかを確かめて，誤っているならなぜ成り立たないかを追えるようにする．

ほかの形式手法との違いはこんな感じ：

有限スコープでの検査：
有限範囲では正しく結果を返すけど，有限なので完全じゃない（スコープを拡大すると反例があるかも）ということが起こる．ほかの手法が定理証明を行うのに対して，Alloy では有限スコープで検査して厳密性を犠牲にする代わりに，定理証明ではなく SAT に置き換えて検査することで，完全じゃないけどお手軽に使える．
モデル内で無限の可能性があってよい：
システムのコンポーネントやそのふるまいを記載することができるけど，その要素の個数に制約はないので，要素はどんどん増やしちゃって OK．
宣言的に書く：
簡単に言うと，処理（のやり方）を書くのではなくて，モデルが満たすべき性質を書くことっぽい．Declarative について参考．
自動で解析：
Z 記法みたいな（場合によっては対話的な）定理証明じゃなくて，スコープ内で自動で検査を行う．（OCL についてはよくわからない！）
構造を持ったデータ：
木構造みたいなデータ構造を表現できるので，いろんな状態を記載できますよ，的な．

ファイルシステムを作っていきまっせ～ということ．ファイルのディレクトリ構造にループがないことを確かめたり，ルートディレクトリの概念がきちんと導尿宇されているかとか，そういうのを調べていくっぽい．
それを，単純な状態から初めて，欠陥を調べたり直したりして進めていきますよ～という言うかんじっぽい．

とりあえずこんな感じ．
次回からチュートリアル始めます！