| 前置 | 调用方必须满足，否则行为未定义 |
|---|---|
| 后置 | 返回时必须成立的保证 |
| 不变量 | 对象生命周期内始终成立 |
约束示例
约束示例
transfer(from, to, amount):
前置：from != to, amount > 0
后置：from.balance + to.balance 不变
不变量：任一账户 balance >= 0不变量与前后置条件（Design by Contract 视角）
把约束写成可检查的三元组：前置条件（调用方义务）、后置条件（实现方承诺）、不变量（对象恒真约束）；写进测试与断言后，重构与扩展时错误更早暴露。
易错点
- 只写文档不写测试：约束无人执行，逐渐失真
- 把不变量当校验点全量运行时检查：热点路径成本高，改抽样与断言
数据来源与参考
- Bertrand Meyer · Design by Contract（Eiffel 语言首次系统化）