物件約束語言（OCL）全面指南

Table of Contents hide

5.2 2. 前置與後置條件（pre, post)

根據所提供的講義資料，本指南涵蓋了物件約束語言（OCL）在UML建模背景下的基本概念、語法及實際應用。

Objct Constraint Language (OCL)

1. OCL簡介

我們為什麼需要OCL？

雖然UML圖表（例如類別圖）在可視化結構方面表現出色，但無法表達規格中所有相關的面向。

自然語言具有歧義性。
傳統的正式語言雖無歧義，但對一般系統建模者而言過於困難，難以閱讀與撰寫。
OCL 彌補了這項差距：它是一種 正式語言 用來表達精確的約束，但仍然保持 易於閱讀與撰寫.

OCL的核心特性

純粹的表示式語言： 表示式不會產生副作用。評估一個OCL表示式會傳回一個值，但無法改變系統的狀態。然而，它能夠描述狀態的改變（例如，在後置條件中）。
並非程式語言： 你無法撰寫程式邏輯、控制流程，或呼叫會改變狀態的程序/作業。
類型語言： 每個表示式都具有類型。合乎格式的表示式必須遵守類型相容規則。每個UML分類器都是OCL的一種類型。
即時評估： 物件的狀態在評估OCL表示式期間無法改變期間 OCL表示式的評估過程中。

2. 基本語法與語義

上下文與Self

每個OCL表示式都是在特定UML分類器（類別、介面等）的上下文中進行評估。

上下文：定義約束所適用的類別。
self：一個保留字，指代正在評估的上下文類別的特定實例。

上下文 Person
-- 'self' 指代 Person 的特定實例

註解與運算子

註解：以表示--（例如，-- 這是一個註解).
中綴運算子：您可以使用標準的數學/邏輯運算子（+, -, =, <）。在概念上，a + b等同於a.+(b).

存取屬性

使用點符號來存取屬性或操作。即使操作沒有參數，也必須使用括號。

上下文 Person
self.age             -- 存取 'age' 屬性
self.stockPrice()    -- 呼叫 'stockPrice' 操作

3. 類型與集合

基本預定義類型

OCL 包含具有特定操作的標準類型：

布林值： true, false (操作： and, or, not, implies, xor)
整數 / 實數： 數字 (操作： +, -, *, /, 絕對值, 最大值, 最小值, 除法, 取模)
字串： 文字（運算： 大小, 串接, 子字串, 轉為整數)

集合

集合是用來儲存多個元素的抽象類型。它們使用 -> 符號來存取。

集合： 數學集合（無重複項目，無順序）。 集合 {1, 2, 5}
有序集合： 無重複項目，但依位置排序。 有序集合 {5, 4, 3}
集合： 允許重複項目，無順序。 集合 {1, 2, 2, 5}
序列： 允許重複項目，有順序。 序列 {1, 2, 5, 10}
- 注意： 這個 .. 符號會建立一組連續的整數： 序列 {1..5}.

關鍵集合運算

常見： size(), isEmpty(), notEmpty(), includes(v), excludes(v), count(v), sum().
迭代器（OCL 的關鍵）：
- select(expr): 返回元素，其中 expr 為真。
- reject(expr): 返回元素，其中 expr 為假。
- collect(expr): 從所有元素中提取特定屬性，並放入新的集合中。
- forAll(expr): 返回 true 如果 expr 對至少一個元素為真。所有元素。
- exists(expr): 返回 true 如果 expr 對至少一個元素為真。至少一個 元素。
- iterate(elem; acc = init | expr): 所有迭代器的通用基礎。

迭代器語法變體：

self.employee->select(age > 50)
self.employee->select(p | p.age > 50)
self.employee->select(p: Person | p.age > 50)

4. 導航 UML 模型

OCL 被廣泛用作導航語言，用於遍歷關聯。

標準導航

使用相反的角色名稱進行導航。返回類型取決於多重性：

多重性 1 或 0..1: 返回單個物件。
多重性 *: 返回一個 集合 （或 有序集合 如果標記為 {有序}).

上下文 Company
self.manager.age > 40               -- manager 是 0..1，返回一個 Person 物件
self.employee->notEmpty()           -- employee 是 0..*，返回一個集合

如果缺少角色名稱，請使用另一端類別的小寫名稱（例如 self.bank).

關聯類別

使用關聯類別的小寫名稱導航至關聯類別。

上下文 Person
self.job->size() >= 1  -- 'job' 是 Person 與 Company 之間的關聯類別

遞歸關聯

當一個關聯迴圈回到同一個類別時（例如，兩個 Person 之間的婚姻），必須使用方括號指定方向 [角色名稱].

上下文 人員
self.marriage[妻子]->select(m | m.結束 = false)->size() = 1

已限定的關聯

使用方括號中的限定符屬性來選擇特定的物件。

上下文 銀行
self.customer[12345]  -- 回傳帳戶編號為 12345 的特定人員
self.customer         -- 回傳所有客戶的集合

重新類型化（轉型）

使用 oclAsType() 來存取子類別或隱藏的超類別屬性。

self.oclAsType(子).p       -- 存取在子類別中定義的屬性 'p'
self.oclAsType(超).p     -- 存取在超類別中定義的屬性 'p'

5. 寫入約束

1. 不變式（`inv`)

必須永遠為所有類別實例為真。

上下文 公司 
inv: self.員工人數 <= 50
inv SME: self.股票價格() > 0  -- 'SME' 是約束的可選名稱

2. 前置與後置條件（`pre`, `post`)

與操作相關的約束。

pre: 必須為真 執行前 執行。
post: 必須為真 執行後執行。使用結果用於返回值。
@pre：用於後置條件中參考屬性的值操作開始前操作開始前。

上下文 Person::income(): Integer
pre adult: self.age >= 18
post resultOK: result < 5000

上下文 Company::hireEmployee(p: Person)
post: employee = employee@pre->including(p)

3. 身體、初始與衍生表示式

body：定義查詢操作的結果（可為遞迴）。
init：定義屬性的初始值。
derive：定義衍生屬性。

上下文 Person::income(): Integer
body: self.job.salary->sum()

上下文 Person::isMarried: Boolean
init: false

上下文 Company::noEmployees: Integer
derive: self.employee->size()

6. 進階 OCL 功能

Let 與 Def 表示式

let：在單一表示式中定義區域變數。

let totHours: Integer = self.worksOn->collect(hours)->sum() in totHours >= 30

def：定義可重複使用的變數或與分類器相關的運算。
```
def: hasTitle(t: String): Boolean = self.job->exists(title = t)
```

未定義值（三值邏輯）

如果子表示式未定義（例如，導航至空關聯），則整個表示式為未定義。然而，布林運算子具有短路例外：

true or <未定義> = true
false and <未定義> = 錯誤
錯誤意味著<undefined> = 正確
<undefined>意味著正確 = 正確

類別功能與預設物件屬性

allInstances(): 回傳一個集合，包含該類別所有存在的實例。
```
Person.allInstances()->size() <= 100
```
物件屬性： oclIsTypeOf(類型), oclIsKindOf(類型), oclInState(狀態), oclIsNew (用於後置條件)。

7. 綜合案例研究：公司模型

為了鞏固這些概念，以下是一組應用於公司資料庫模型（員工、部門、專案、依賴者）的完整性約束。

基本屬性約束

-- 年齡必須大於等於18
context Employee inv: self.age() >= 18

-- 雇用日期必須在出生日期之後
context Employee inv: self.hireDate > self.birthDate

-- 管理者開始日期必須在雇用日期之後
context Employee inv: self.manages->notEmpty() implies self.manages.startDate > self.hireDate

導航與關係約束

-- 主管必須比員工年長且薪資更高
context Employee 
inv: self.supervisor->notEmpty() implies self.age() > self.supervisor.age()
inv: self.supervisor->notEmpty() implies self.salary < self.supervisor.salary

-- 主管必須在下屬之前被雇用
context Employee 
inv: self.subordinates->notEmpty() implies self.subordinates->forall(e | e.hireDate > self.hireDate)

-- 部門經理必須是該部門的員工
context Department 
inv: self.worksFor->includes(self.manages.employee)

-- 專案地點必須是部門的其中一個地點
context Project 
inv: self.controls.locations->includes(self.location)

-- 員工只能參與其部門所控制的專案
context Employee 
inv: self.worksFor.controls->includesAll(self.worksOn.project)

集合與迭代器約束

-- 社會安全號碼必須在所有員工中唯一
context Employee 
inv: Employee.allInstances->forAll(e1, e2 | e1 <> e2 implies e1.SSN <> e2.SSN)

-- 依賴者的姓名與關係必須在每位員工中唯一
context Employee 
inv: self.dependents->forAll(e1, e2 | 
      e1 <> e2 implies (e1.name <> e2.name or e1.relationship <> e2.relationship))

-- 衍生屬性：部門中的員工人數
context Department 
inv: self.nbrEmployees = self.worksFor->size()

-- 員工最多只能參與4個專案
context Employee 
inv: self.worksOn->size() <= 4

使用複雜邏輯`讓`和`選擇`

-- 每週總工作時數必須介於30至50小時之間
上下文 員工 
不變式: 讓 totHours: 整數 = self.worksOn->收集(小時)->總和() 
     在 totHours >= 30 且 totHours <= 50

-- 在特定專案上，最多僅有2名員工工作少於10小時
上下文 專案 
不變式: self.worksOn->選擇(小時 < 10)->大小() <= 2

-- 僅部門經理可於專案上工作少於5小時
上下文 員工 
不變式: self.worksOn->選擇(小時 < 5)->非空() 意味著 
     self.worksFor.manages.employee = self

-- 無下屬的員工必須在所有其負責的專案上工作至少10小時
上下文 員工 
不變式: self.subordinates->為空() 意味著 self.worksOn->對所有(小時 >= 10)

-- 部門經理必須在部門所管控的所有專案上工作至少5小時
上下文 部門 
不變式: self.controls->對所有(p: 專案 | 
      self.manages.employee.worksOn->選擇(小時 >= 5)->包含(p))

防止循環（遞迴邏輯）

-- 員工不能監督自己
上下文 員工 不變式: self.subordinates->排除(self)

-- 監督階層不得形成循環
上下文 員工 
定義: allSubordinates = self.subordinates->聯合(
          self.subordinates->收集(e: 員工 | e.allSubordinates))
不變式: self.allSubordinates->排除(self)