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

Question

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

{P} x= x-x；{x'=x}

P: x=0

{true} y= y-y；{Q}

问:Y=0

编辑：

我首先应用this，如下所示：

{ true } y=y-y {Q} ==> sp(y = y-y；true) =∃x，y= x-x∧true

现在我不确定如何处理它；在我看来，"y = 0“最有意义，但这似乎并不正确。

Answer 1

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

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

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