如何導出循環不變式？

Question

給出以下代碼片段，其中x是一個數字。

{ y >= 0 } 
z = 0 
n = y 
while (n > 0) begin 
z = z + x 
n = n – 1 
end 

它計算什麼？證明它，展示如何導出循環不變式。

我該怎麼做？

Answer 1

對於給定X和Y它計算X * Y。

在開始時，Z的值爲零，而N = Y（循環的變量將在我們的循環中倒計時）。

該循環執行Y次，並在每次執行時，累積X到Z。

最後，當N達到0時，循環將終止，那麼Z的值應爲X * Y。

Answer 2

這個例子被稱爲最正確的程序，因爲它在每個軟件驗證過程中都被證明。下面是該方案與不變量上的每一步上市：

{ y >= 0 } z = 0 // invariant: z = 0 n = y // invariant: n = y and z = 0 while (n > 0) begin // loop invariant: y * x - n * x = z z = z + x n = n – 1 end // Final invariant: n = 0 and y * x = z

在my paper page 118提供了這個例子所有的理論細節。