哪个 hoare-triples 是正确的？

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

我本来打算发表评论，但我没有评论的声誉。
这两个 hoare-triples 肯定不是等价的。如果 p0 >= balance，则第一个三元组的右侧评估为 true，而第二个三元组的右侧评估为 false。我在工作，现在不知道哪个是正确的 hoare-triple，但我相信比我更有资格的人会在我完成工作之前回答。

如果我们让 P := p0 Q) v (-P => R) 和 (P ^ Q) v (-P ^ R)，并创建如下真值表。

+---+---+---+----------------------------+-- -------------------+
| .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)，因为这两个语句都必须成立。我是新手，知识渊博的人可能会纠正我。