Hoare邏輯：嚴格降低循環變量本身如何證明終止？

參照while rule for total correctness，WP似乎告訴我，找到嚴格減少的循環變體足以證明終止。我無法接受，因爲我錯過了某些東西或者規則是錯誤的。考慮Hoare邏輯：嚴格降低循環變量本身如何證明終止？

int i = 1000; 
while(true) i--;

其中變量i的值是嚴格遞減的循環變種，但環肯定不會終止。

當然規則需要有一個附加的先決條件，如事我< 0→¬B（其中乙處於公理模式循環條件），使得循環條件最終「捕獲」循環變並退出。

或者我錯過了什麼？

來源

2011-05-31 jameshfisher

循環變量必須是自然數。自然數不能減少過零。使用大詞彙，循環變體是一個相對於有根的關係單調遞減的值。這是你的推理所缺少的有根有據。

來源

2011-05-31 15:12:52

或者換句話說，'i'並不是我認識的任何語言的嚴格遞減變體 - 在大多數情況下，它會達到最小值，然後繞回（即變大）或觸發未定義的行爲（可能會終止循環，你永遠不知道）。也許在某些真實的情況下，假設我們可以認爲'int'是某種語言中的一個bignum，在這種情況下n.m.的完整解釋是必需的 - 它正在減少，但對於一個良好的秩序而言不是。 – 2011-05-31 15:33:18

@Steve它也不一定，請參閱[bignum]（http://en.wikipedia.org/wiki/Bignum）。如果你有一臺Linux機器，在終端上鍵入'bc'。在那裏，你有一種無限精確的編程語言在你的指尖。 – 2011-05-31 15:39:17

非常簡單的答案，謝謝你。 – jameshfisher 2011-05-31 16:12:54

作爲維基百科文章中指出：

[...]的條件乙必須暗示噸是不是它的範圍，的最小元件對本否則前提規則將是錯誤的。

在手邊的情況下，乙是true和噸是i。 true對i的最小性沒有影響，所以不符合規則的前提。

來源

2011-05-31 17:55:50 WReach

你引用的文本暗示了變量從一次迭代到下一次迭代嚴格減少，這不在OP的例子中。（根據語言，OP的例子調用UB或在某個步驟增加2^32-1。） – 2011-06-08 00:56:22

通常的排序「<」在自然數上是有根據的，但不是整數。爲了使關係有根據，其域的每個非空子集必須具有最小元素。既然可以證明，關於一個有根的關係沒有無限下降鏈，那麼帶有變體的循環必須終止。

當然，在最小元素的情況下，循環的條件必須是假的！

然而，變體不需要限制在自然數。超限定序也是有序的。

來源

2011-08-18 05:06:51 JustinL

Hoare邏輯：嚴格降低循環變量本身如何證明終止？

回答

相關問題