C++26 合约：前置条件和后置条件简介

合约与形式化验证的作用

• 许多人认为 C++26 合约是一种编码 Hoare 三元组（前置/后置/不变式）并生成可由工具/求解器检查的验证条件的方法。
• 来自其他生态（Racket、SPARK/Ada、专门的 C/C++ 验证器）的例子被引用为证据：即使完整的 C++ 永远做不到，受限子集也可以被静态证明。
• 合约可以帮助隔离“棘手”的函数：在假定前/后置条件成立的前提下证明其余部分，并将证明失败的位置局部化。

---

运行时行为与输入验证

• 普遍共识：合约用于“这种事绝不能发生；如果发生了，那就是 bug”，而不是用于常规用户输入验证。
• 几位参与者指出，“输入验证”和“假设”之间的边界很模糊，实际中很可能被误用。
• 合约被拿来与 assert 比较：作用相似，但标准化、在声明处可见，并支持多种求值模式（ignore、observe、checking）。
• 批评主要集中在“幽灵代码”模型：你必须假定检查可能被省略，因此不能把它们作为安全关键行为的依据。

---

优化与性能

• 有人希望编译器能把合约像 assume 一样用于优化，或消除冗余检查；也有人表示这并不是主要设计目标。
• 令人失望的是，在当前实现中，“ignore” 模式（不做运行时检查）似乎并不会继续指导优化。
• 嵌入式和高性能开发者喜欢能够在工作站上启用检查，而在目标构建中关闭它们。

---

放置位置、头文件与模块

• 关于把合约放在哪里存在争论：放在头文件里能把它们作为文档暴露出来，但可能迫使引入大量头文件；放在 .cpp 文件里则避免了这一点，但会失去可见性。
• 标准要求首个声明必须携带合约，这推动使用方式偏向头文件；有人认为模块将缓解编译时间膨胀。
• 建议的模式：让头文件中的合约保持简单，或委托给在别处定义的辅助函数。

---

语言复杂性与对比

• 有些人认为 C++ 已经过于庞大，合约只是带来更多复杂性而收益有限；另一些人则认为这只是对长期使用模式的正式化。
• 讨论中还比较了 Eiffel、D、Clojure、Racket、Rust、Go：许多其他语言都有合约或前/后置设施，但在实际可用性上体验各不相同。

---

实用性、安全性与工具链

• 支持者强调它对 IDE、静态分析器、AI 代理以及作为精确的“可执行文档”的价值。
• 怀疑者认为合约“只是更花哨的 assert”，不能保证执行，某些模式下甚至可能比普通 assert 更不安全。
• 总体来看：人们对工具与验证潜力持谨慎乐观态度，但对其在日常实践中的收益以及设计取舍则相当怀疑。