loops - 如何导出循环不变量？

Question

给定以下代码片段，其中 x 是一个数字。

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

它计算什么？证明它，展示如何推导出循环不变量。

请问我该怎么做？

Answer 1

这个例子被称为最正确的程序，因为它在每个软件验证课程中都得到了证明。以下是每一步都有不变量的程序列表：

{ 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

这个例子的所有理论细节都在我的论文第 118 页中提供。

Answer 2

对于给定X，Y它计算X * Y.

一开始， 的值Z为零，而N = Y（循环的变量将在我们的循环中倒计时）。

循环执行Y次数，每次执行时，它都会X将Z.

最后，当N达到 0 时循环将终止，那么 的值Z应该是X * Y。