formal-verification - Hoare Triples - 最弱前置条件/​​最强后置条件

Question

对于最弱的前置条件和最强的后置条件，这是正确的吗？

{P} x = xx; {x'=x}
P: x = 0

{真} y = yy; {Q}
问：y = 0

编辑：

我开始应用它如下：

{true} y = y - y {Q} ==> sp(y = yy; true) = ∃x,y = xx ∧ true

现在我不知道该怎么办；在我看来，“y = 0”最有意义，但这似乎不正确。

Answer 1

前置条件越强，后置条件越强。例如，

{y = 5} x := 8 {x = 8; y = 5}

如果前置条件是最弱的，即true，则没有关于y后置条件中的值的有效假设。