監訳者序文
日本語版に寄せて
序文
謝辞
第1章　はじめに
第2章　ざっと一巡り
2.1 静的な側面：状態を調べる
2.2 動的な側面：操作を追加する
2.3 階層の導入
2.4 実行トレース
2.5 まとめ
第3章　論理系
3.1 3つの側面を持つ論理系
3.2 アトムと関係
3.3 スナップショット
3.4 演算子
3.5 制約
3.6 宣言制約と多重度制約
3.7 濃度制約と整数
第4章　言語
4.1 例題：自分が自身の祖父
4.2 シグネチャとフィールド
4.3 モデル図
4.4 型と型検査
4.5 ファクト、述語、関数、アサーション
4.6 コマンドとスコープ
4.7 モジュールと多相性
4.8 整数と算術演算
第5章　解析
5.1 スコープを網羅する解析
5.2 インスタンス、充足例、反例
5.3 非限定の全称限量子
5.4 スコープの選択と単調性
第6章　事例
6.1 リーダー選出問題
6.2 ホテルの客室施錠
6.3 メディア資産管理
6.4 メモリの抽象化
付録A　練習問題
A.1 論理の問題
A.2 単純なモデルを拡張する
A.3 古典的パズル
A.4 メタモデル
A.5 小さなケーススタディ
A.6 自由形式のケーススタディ
付録B　Alloy言語リファレンス
B.1 字句
B.2 名前空間
B.3 文法.
B.4 優先順位と結合性
B.5 意味論の基本
B.6 型とオーバーロード
B.7 言語機能
B.8 関係式
B.9 整数式
B.10 ブール式
付録C　中核の意味論
C.1 Alloy の中核の意味論
付録D　図的記法
付録E　Alloy以外の手法
E.1 事例
E.2 B
E.3 OCL
E.4 VDM
E.5 Z
付録F　Alloy Analyzerクイックガイド
F.1 Alloy 解析器の起動
F.2 Alloy 解析器のGUI
F.3 Alloy モデルの解析を行う
F.4 Alloy 4の構文的機能
付録G　訳語一覧
参考文献
訳者あとがき
索引