霍爾邏輯證明

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

如果你仔細閱讀這本書，你會看到福樂規則選擇語句如下：

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

您可以在書中找到很明顯的事實是

該行上面的第一個邏輯語句表示，然後是子句; 第二個代表其他子句。

所以，如果你只有然後部分規則更改爲

{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 > 0} 

相等於

{n < 0} 

這反過來又滿足的先決條件。

聲明

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

顯然是正確的了。 那麼，我們已經確保這條線上面的兩條語句都是正確的，所以下面的語句也是正確的。