5章オブジェクト指向デザインを検査する

5.1 クラス図とOCL

5.1.1 オブジェクト指向ソフトウェアとUML

省略

5.1.2 静的な情報構造

OCL: Object Constraint Language

(1) クラス図への注釈

salary, budgetは正の数
Departmentには少なくともProjectの数のEmployeeがいる
多くのProjectに従事するEmployeeはより多くのsalaryを得る 4. ProjectのbudgetはDepartmentのbudgetを超えない
Projectに従事するEmployeeはそのProjectを管理するDepartmentに属する

P.104上～

(2) Alloyによる表現と解析例

P.104下～

invDepartment: 2を表している

invEmployee: 1を表している

invProject: 4,5を表している

P.106中～

所属の関係を表す

P.107上～

budgetの条件を満たさないことが分かる

5.1.3 メソッドの機能振る舞い

(1) 状態ベース仕様

プロジェクトへの人員追加メソッド

事前条件：
- プロジェクト人数の上限を超えない
- 当該プロジェクトに関わっていない
- 所属部門管轄のプロジェクトであること

事後条件：
- その人がそのプロジェクトに従事
- その人の給料が増加

P.107下～

P.108上～

3.(給料)と4.(予算)の競合が見えてくる

→ プログラミングの前に仕様の問題が明らかになった

(2) Alloyによる記述例

5.1.2とは違う表し方で

P.108下～

i2: 2を表している

m1: Employeeどこかに所属する

m2: Projectはどこかの管理下

i3: 3を表している

i4: 4を表している

i5: 5を表している

P.109下～

t1: i5では十分でない所がある（？）

P.110上～

preState: 事前条件

postState: 事後条件

P.110下～

Separated: 事前と事後の区別

FrameCondition: 操作に関係ない所は変わらない

P.111上～

[ex8-3] 教科書5章の例題について、次の内容はどこに表現すべきですか：Projectのbudget < Departmentのbudget

[ex8-4] 教科書5章の例題について、次の内容はどこに表現すべきですか：Projectには複数のEmployeeが所属する

[ex8-5] 教科書5章の例題について、次の内容はどこに表現すべきですか：新しいProjectに参加したら給料が上がる

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

一覧に戻る

5章 オブジェクト指向デザインを検査する