目前我正在研究霍尔逻辑以了解程序的正确性。特别是，我正在阅读 Hoare logic我正在分析 while 规则中的以下示例:
我想知道的是简化步骤:为什么 {x <= 10 ^ x < 10}简化为 {x < 10}而不是 {x <= 10} ？
最佳答案
声明说:“Condition1 AND Condition2”，其中 Condition2 ( < ) 比 Condition1 ( <= ) 更具限制性。
当然，满足两者(由于“AND”)的任何事物也必须满足更严格的条件。
因此，仅使用限制性更强的条件本身就足够了。另一个条件是多余的。
换句话说:<= 之间的唯一区别和 <是 ==案件。没有什么能满足 == case 可能满足更严格的 <大小写，所以没有必要检查它。
此外，您可能需要查看 https://math.stackexchange.com/对于纯数学/逻辑问题。
关于algorithm - 为什么 {x <= 10 ^ x < 10} 简化为 {x < 10} 而不是 Hoare 逻辑中的 {x <= 10}？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/38964203/