2.2 Alloyの基礎

2.2.1 関係の論理の考え方

(1) 概要

1階述語論理では表現力低い

→ 推移閉包オペレータで補っている

(2) 基本的な概念要素

例： {(A,B), (C,D)}

P.30上～

スカラーの例： {(A)}

P.30上～

プロダクト

{(A),(B)}->{(C)} = {(A,C), (B,C)}

P.30下～

ジョイン

{(A,B)}.{(B,C)} = {(A,C)}

P.31中～

推移閉包

^r = r + r.r + r.r.r + ..

2.2.2 解析の方法

(1) SAT問題への変換

run で S and P を調べる

P.32上～

check で S and not Q を調べる

P.32下～

スコープが小さい → もれる恐れ

スコープが大きい → 結果が得られない恐れ

[ex3-1] {(A,B), (C,D)}という記述で表せてないものはどれですか

[ex3-2] {(A,B)}.{(B,C)} = {(A,C)} で表現できる内容はどれですか

(2) 命題論理式への変換

forall = and..and

exist = or..or

P.33中～

スコーレム定数： exist を無くす考え方

2.2.3 有界モデル発見の限界

P.34下～

P.35下～

P.35下～

2.3 Alloyとその周り

（省略）

[ex3-3] 素数とそうでない数は交互にある、という命題について、3からいくつまでスコープを広げたら偽になるか

[ex3-4] 自然数を対象として次の命題のうち、有限スコープで検証できるのはどれですか

課題

教科書（図はすべてこちらより引用）：
　中島震，「形式手法入門―ロジックによるソフトウェア設計―」，オーム社