correctness - 后置条件中具有未知变量的霍尔三元组

Question

我正在推理 Hoare Logic 的练习。

我应该找到满足三元组的所有布尔表达式B和所有程序S，假设 的评估不能修改存储，但执行可以修改它并改变 的值。P{true} if B then S; if B then P; {a >= 0}BSB

特别是，我不知道我能说什么a，因为它只存在于后置条件中，我从未找到过这样的例子。

谢谢你的帮助！

Answer 1

（我之前的回答是错误的。）

这个问题有点开放式，因为有无限数量的表达式 ( B) 和程序 ( Sand P) 满足三元组。此外，三元组足够复杂，可以防止将任务简化为简单的通用答案。

基本上你可以把它分解如下：

• 对于所有B为假的状态，a >= 0必须保持（否则整个三元组不能保持）
• B对于是的州true，程序S; if B then P必须确保a >= 0
• 这适用于所有人S，B这样P......
  • 要么S是B假的，要么a >= 0
  • 或者，S使B真实，并且...，

等等