内容紹介
Alloy(アロイ)を通じて形式手法を学ぶ
形式手法は、高度な信頼性が求められるソフトウェアの開発で利用されてきた、数学に基づく開発技術です。Alloy(アロイ)は、形式手法を誰もが実践できることを目指したツールであり、テストでは排除できないソフトウェアの欠陥について検証するためのものです。
本書は、"Software Abstractions: Logic, Language, and Analysis"の翻訳書です。Alloyによるさまざまな事例のモデリングを通じ、「アジャイルで軽量な形式手法」ともいえる技術を学びます。
目次
主要目次
監訳者序文
日本語版に寄せて
序文
謝辞
第1章 はじめに
第2章 ざっと一巡り
第3章 論理系
第4章 言語
第5章 解析
第6章 事例
付録A 練習問題
付録B Alloy言語リファレンス
付録C 中核の意味論
付録D 図的記法
付録E Alloy以外の手法
付録F Alloy Analyzerクイックガイド
付録G 訳語一覧
参考文献
訳者あとがき
索引
詳細目次
監訳者序文
日本語版に寄せて
序文
謝辞
第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 訳語一覧
参考文献
訳者あとがき
索引
続きを見る