霍尔逻辑证明

Question

给出以下内容正确的证明。

{n != 0}    
if n<0 then 
n= -n 
{n>0} 

以下推理规则应该有助于

{B and P} S {Q}, (not B) and P=>Q 
---------------------------------
{P}if B then S{Q} 

我一直在网上寻找一个明确的解释，或者至少是一个可以效仿的例子，但我不太明白，我在下面找到了一些可能有帮助的网站，但没有任何例子。

第148-160页

非常感谢任何帮助，我希望看到这个问题得到解决，这样我就可以解决其他问题，我很困，书中没有任何例子。

这些链接也可能会有所帮助。谢谢，10分！

http://en.wikipedia.org/wiki/Hoare_logic#Conditional_rule

Answer 1

如果你仔细阅读这本书，你会发现选择语句的fule规则看起来像：

{B and P} S1 {Q}, {(not B) and P} S2 {Q}
--------------------------------------
{P} if B then S1 else S2 {Q}

你可以在书中找到一个很明显的事实，

该行上方的第一个逻辑语句表示then子句；第二个表示else子句。

因此，如果您只有部分，则规则将更改为

{B and P} S {Q}, {not B and P} {Q}
--------------------------------------
{P} if B then S {Q}

这是非常合乎逻辑的规则。当且仅当B为真时，您将到达序列S。因此，您可以将其添加到前置条件语句中。

在您的情况下，推理规则看起来像：

{n < 0 and n != 0} n = -n {n > 0}, {n >= 0 and n != 0} {n > 0}
--------------------------------------------------------------
{n != 0} if n < 0 then n = -n {n > 0}

若我们证明了线上的逻辑语句，我们将证明线下的语句。

报表

{n < 0 and n != 0} n = -n {n > 0}

可以通过赋值公理来证明，该公理可以在书的第150页找到。

n = -n {n > 0}

我们必须用后条件中的n=-n替换n。所以我们有

{-n > 0}

等于

{n < 0}

这又满足了前提条件。

报表

{n >= 0 and n != 0} {n > 0}

显然也是正确的。好吧，我们已经确保了行上的两个语句都是正确的，所以行下的语句也是正确的。