Assumptions weaken properties
16 hours ago
- 性质/测试的强度通过逻辑蕴含来定义：更强的性质保证更弱的性质。
- 向规约添加假设总会使结果性质变弱，形式化为：Prop ⇒ (Assumption ⇒ Prop)。
- 假设较少的系统更健壮，适用范围更广（例如，Unicode JSON 解析器与仅支持 ASCII 的解析器相比）。
- 依赖假设的三个常见原因：强性质无法实现、成本过高或难以直接验证。
- 大多数假设涉及外部“外程序”因素（环境、硬件、用户输入），这使得它们的验证与系统逻辑的验证截然不同，通常也更困难。