1

假设有一个方法接受两个参数 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))

（=> 是暗示）我想知道哪个是正确的？或者两者都是正确的？

4

1 回答 1

2

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

如果我们让 P := p0 < balance，Q := balance = b0 - p0 和 R := balance = b0，我们可以用 (P => 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)，因为这两个语句都必须成立。我是新手逻辑，知识渊博的人可能会纠正我。

于 2017-01-10T19:36:28.310 回答