假設你接手一個銀行系統，發現 `BankAccount` 介面：
interface BankAccount {
float getBalance();
float deposit(float amount);
float withdraw(float amount);
}
問題叢生：`amount` 可為負數或零嗎？允許透支 (負餘額) 嗎？參數錯誤時拋何種異常？傳統單元測試 (JUnit) 雖能驗證行為，但屬於**外部測試代碼**，與介面定義分離，難以作為強制性契約。契約式設計 將前置條件、後置條件、不變條件**內嵌於介面/類別中**，成為可執行、可驗證、可文檔化的正式規範。
Contract4J 是開源工具，使用 Java 5 `@Annotation` 宣告契約，執行時透過 **AspectJ 切面** 織入檢查邏輯。失敗即刻終止程式並拋出診斷訊息，強制開發者即時修復邏輯錯誤 (非業務異常處理)。
@Contract
@Invar("$this.balance >= 0.0") // 類不變條件：餘額不得為負
interface BankAccount {
@Post("$return >= 0.0")
float getBalance();
@Pre("amount >= 0.0")
@Post("$this.balance == $old($this.balance) + amount && $return == $this.balance")
float deposit(float amount);
@Pre("amount >= 0.0 && $this.balance - amount >= 0.0") // 禁止透支
@Post("$this.balance == $old($this.balance) - amount && $return == $this.balance")
float withdraw(float amount);
}
| 關鍵字 | 含義 | 適用範圍 |
|---|---|---|
| $this | 被測試物件 (當前實例) | 所有契約 |
| $return | 方法回傳值 | @Post |
| $args[n] / 參數名 | 第 n 個參數 / 具名參數 | @Pre, @Post |
| $old(expr) | expr 在方法執行前的值 | @Post, @Invar |
| $target | 欄位不變條件專用 (可用 $this.field) | @Invar (欄位) |
預設契約：未宣告時自動套用 — 非基本型參數/回傳值不為 null、欄位不為 null。
範圍限制：僅檢查 public/protected/包可見方法與欄位。private 方法、static 方法目前不支援 (理論限制，未來可能開放)。
Contract4J 不僅是工具，更展示了 **Aspect-Oriented Design 新趨勢**：
這與 **Hibernate/EJB3 持久化註解**、**Spring `@Transactional`** 同一設計模式：註解承載元資料，切面/框架解讀執行。
切面本質橫切系統，擁有修改物件狀態的強大權力，引發完整性、健壯性、可理解性疑慮。學界/業界正探索：**切面介面應包含「契約資訊」，限定切面可對元件做何種修改** (如：禁止狀態修改、禁止切入關鍵區域、效能/安全邊界)。元件透過介面「授權」切面可存取的連接點與狀態，切面僅透過授權介面織入 — 耦合更穩定，系統演化更可控。
Contract4J 以直觀的 Java 5 註解，將契約式設計從理論帶入實戰。它利用 AspectJ 強大織入能力，卻不要求開發者精通 AOP。契約即文檔、即測試、即防禦性程式設計的執行守則。在邏輯錯誤難以用單元測試覆蓋 (如 EJB2、複雜整合邏輯) 的場景，Contract4J 是極佳補強。嘗試在下個專案引入，你會發現「介面不再說謊」的安心感。
