不变量与前后置条件是什么

把约束写成可检查的三元组：前置条件是调用方必须满足的义务，后置条件是实现方给出的承诺，不变量是对象在整个生命周期内恒真的约束。这是 Design by Contract 的基本视角（Bertrand Meyer 在 Eiffel 中系统化）。把三者写进测试与断言后，重构与扩展时错误会更早暴露，而不是等到数据出问题才发现。

基本信息

常见的可写约束

• 转账金额必须为正，且转出与转入账户不同
• 转账前后两边余额之和保持不变（守恒量）
• 账户余额任何时刻不得为负
• 购物车条目数不超上限，金额合计等于各项之和
• 状态机只允许沿合法边迁移（草稿 → 已提交 → 已支付）
• 时间区间必须满足开始早于结束

约束示例

transfer(from, to, amount):
  前置：from != to
        amount > 0
        from.balance >= amount
  后置：from.balance + to.balance 不变
        from.balance >= 0 且 to.balance >= 0
  不变量：任一账户 balance >= 0

# 落地：前置作为参数校验，后置与不变量写进断言与测试
assertThat(from.balance().add(to.balance()))
    .isEqualTo(balanceBefore);

三者对照