Hoare邏輯循環不變式

Question

我在看Hoare Logic，並且在理解找到循環不變的方法時遇到了問題。

有人可以解釋用於計算循環不變的方法嗎？

什麼循環不變應該包含一個「有用」的？

我只處理簡單的例子，發現不變量並證明部分和完全校正的例子，如：

{ i ≥ 0 } while i > 0 do i := i−1 { i = 0 } 

Answer 1

如果我們談論的是霍爾的邏輯對證明的程序（部分）的正確性，那麼你使用的前提和後置條件，分解程序並使用霍爾的邏輯推理系統的規則創建和證明感應式。

在你的榜樣，你要使用規則

{p} while b do S {p^not(b)} <=> {p^b} S {p} 

在你的情況下分解程序

• 號碼：I≥0
• B：I> 0
• S：我：= i-1。

所以在下一步我們推斷{i ≥ 0^i > 0} i := i−1 {i ≥ 0}。這可以進一步推斷和證明相當容易。 我希望這可以幫助。

Answer 2

是有用的（爲你的推理）是不變的要點。所以，看看你想要證明的後置條件，並試圖構成一個不變條件，這將有助於你逐步達到後置條件，並且可以從循環的代碼中推導出來。

Answer 3

我不知道這是否會回答你的問題，但萬一它：

• A「循環不變」非正式的是和之前的迭代之後仍是如此陳述事實循環。它基本上定義了程序關於該循環的一致性約束。
• 我不太瞭解Hoare Logic如何精確地告訴你循環不變量是如何計算的，但我懷疑這樣的事情將取決於被分析代碼的語言而不是形式化的證明語言本身。你有正在使用的正式算法描述嗎？我可能能夠進一步提供更多的背景。
• 有用的循環不變將描述特定於應用程序狀態的內容。例如，如果您正在編寫Insertion Sort，則對於主元素運動循環而言，有用的循環不變將基本上聲明該（子）列表在循環執行之前和之後包含相同的對象集合，並且可能以前的元素在排序順序保持排序順序。