『抽象によるソフトウェア設計』

https://gyazo.com/12d3b254c5df4f48db309cb140cf9682

2011/7/15

Alloyの解説書

各節に議論という節があり、そこにQ&Aのようなものが列挙されている

監訳者序文

日本語版に寄せて

序文

抽象的なモデリングに軸足を置く

第1章 はじめに

抽象を思いつきコードに落としても、コードに落とす中でその抽象構造の歪さに気づきがち

自然言語は曖昧すぎ、かといってコードは冗長すぎ

他のものを知らないのでどう特殊なのかわからない

ここから入門して良いのかやや不安はあるが、思想的には好みなのでまあええか

第2章 ざっと一巡り

メールクライアントのアドレス帳を設計する

メールアドレスにエイリアスをつけられる

グルーピング機能がある

家族のアドレスをまとめるなど

2.1 静的な側面：状態を調べる

いったんグルーピング機能を無視する

状態の具体例をインスタンスとして生成

https://gyazo.com/291e7e7e22b03816770c0523f0134560

インスタンスだから、記述を満たしてるなら任意の図が出る感じなのか？

そもそもShowボタンを押せば良のかどうかすらわかってない

Execute押した後の、右側に表示される「instance」かな、一緒か、わからん

つまり、「Bookに載ってるName」が1より多い、ということか

2.2 動的な側面：操作を追加する

動的な振る舞い、制約の追加、モデル化、シミュレーション、性質の検査

2.3 階層の導入

アドレス帳の状態を作り込む、グルーピングもエイリアスもできる

2.4 実行トレース

トレースでモデルを拡張、一連の操作からなる実行列を解析、シミュレーション

2.5 まとめ

第3章 論理系

論理系の3つの側面

述語論理

関係名と限量変数からなるタプル

code:例.alloy

all n: Name, d,d2: Address |

n -> d in address and n-> d2 in address => d = d2

ナビゲーション形式

navigation expression

式は集合を表す

集合は、限量変数から関係を辿ってnavigationすることにより作られる

code:例.allloy

all n: Name | lone n.address

表現力が最も高い

関係計算

relational calculus

式は関係を表す

限量子は使わない

code:例.alloy

no ~address.address - iden

3つの中では比較的簡潔に書ける

「関数的」と「単射的」という用語の導入

この「単射的」は数学の「単射」とは意味が異なる

「関数的」は、写像の定義を満たしているということ

第4章 言語

4.1 例題：自分が自身の祖父

4.4 型と型検査

型の階層

自明に(常に)空集合な式を書くとエラーにしてくれる

4.5 ファクト、述語、関数、アサーション

4.6 コマンドとスコープ

4.7 モジュールと多相性

ぱらよみ

第5章 解析

5.1 スコープを網羅する解析

5.2 インスタンス、充足例、反例

5.3 非限定の全称限量子

5.4 スコープの選択と単調性

第6章 事例

6.1 リーダー選出問題

alloy6で書き直したもの

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.4 Alloy 4の構文的機能

省略記法など

付録G 訳語一覧

参考文献

訳者あとがき

索引