哪个三元组是正确的？

Question

假设有一个方法接受两个参数 balance 和 price，它只执行以下操作：

if(price < balance) {
    balance = balance - price;
}

我觉得有两种可能的写法：

(| price=p0 ^ balance = b0 |) buy (| ((p0 < balance) => balance = b0 - p0) v ((p0 >= balance) => balance = b0) |)

或

(| price=p0 ^ balance = b0 |) buy (| ((p0 < balance) ^ (balance = b0-p0)) v ((p0 >= balance) ^ (balance = b0))

( => 是蕴涵) 我想知道哪个是正确的？或者两者都正确？

Answer 1

我打算对此发表评论，但我没有发表评论的名誉。
这两个霍尔三元组当然不相等。如果 p0 >= balance，则第一个三元组右侧的计算结果为真，而第二个三元组右侧的计算结果为假。我在工作，现在无法计算出哪个是正确的 hoare-triple，但我相信在我完成工作之前会有比我更有资格的人回答。

如果我们让 P := p0 < balance，Q := balance = b0 - p0 和 R := balance = b0，我们可以用 (P => Q) v ( -P => R) 和 (P ^ Q) v (-P ^ R)，并创建以下真理 table.

+---+---+---+----------------------------+--- ----------------------+
| .P |问 | .R | (P => Q) v (-P => R) | (P ^ Q) v (-P ^ R) |
+---+---+---+----------------------------+-------- --------------+
| .T | .T | .T | . . . . . . . .吨。 . . . . . . . | . . . . . . .T. . . . . . . |
| .T | .T | .F | . . . . . . . .吨。 . . . . . . . | . . . . . . .T. . . . . . . |
| .T | .F | .T | . . . . . . . .吨。 . . . . . . . | . . . . . . 。F 。 . . . . . . |
| .T | .F | .F | . . . . . . . .吨。 . . . . . . . | . . . . . . 。F 。 . . . . . . |
| .F | .T | .T | . . . . . . . .吨。 . . . . . . . | . . . . . . .T. . . . . . . |
| .F | .T | .F | . . . . . . . .吨。 . . . . . . . | . . . . . . 。F 。 . . . . . . |
| .F | .F | .T | . . . . . . . .吨。 . . . . . . . | . . . . . . .T. . . . . . . |
| .F | .F | .F | . . . . . . . .吨。 . . . . . . . | . . . . . . 。F 。 . . . . . . |
+---+---+---+----------------------------+-------- --------------+

这表明两个方程不等价。

我猜想右边的正确值应该是 (P => Q) ^ (-P => R)，因为这两个陈述都必须成立。我是 hoare-logic 的新手，知识渊博的人可能会纠正我。

哪个三元组是正确的？

Which hoare-triples is correct?

logic

hoare-logic