给定以下代码片段，其中 x 是一个数字。
{ y >= 0 }
z = 0
n = y
while (n > 0) begin
z = z + x
n = n – 1
end
它计算什么？证明它，展示如何导出循环不变量。
请问我该怎么做？
【问题讨论】：
标签： loops loop-invariant
这个例子是众所周知的最正确的程序，因为它在每个软件验证课程中都得到了证明。以下是每一步都有不变量的程序列表：
{ 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 中提供了此示例的所有理论细节。
【讨论】：
对于给定的X 和Y，它计算X * Y。
一开始，Z 的值为零，N = Y（循环变量，将在我们的循环中倒计时）。
循环执行Y 次，并且在每次执行时，它将X 累积到Z。
最后，当N达到0时循环将终止，那么Z的值应该是X * Y。
【讨论】：