计算阶乘函数的循环不变式
我很难正确识别以下函数的循环不变量：
F(y)
X <-- 1
while (y > 1)
do x <-- x * y
y <-- y - 1
return (x)
我已将循环不变量识别为 x = 1 OR x = y！ ，因为该语句作为预条件成立条件并作为后置条件成立。
它似乎并不适用于每次迭代，例如，如果 y = 3，则在循环的第一次迭代中，x = 1 * 3 等于 3 而不是 3！等于 6。
我想这就是我真正困惑的地方。一些书籍文章指出，循环不变量是一个在开始或循环时必须等于 true 的语句（因此是前提条件），并且在循环结束时也必须保持 true （因此是后置条件），但不一定需要在循环的中途保持 true。
上述函数的正确循环不变量是什么？
I'm having a hard time correctly identifying a loop invariant for the following function:
F(y)
X <-- 1
while (y > 1)
do x <-- x * y
y <-- y - 1
return (x)
I've identified the loop invariant to be x = 1 OR x = y! as that statement holds true as a pre-condition and holds true as a post-condition.
It doesn't seem to hold true for every iteration, as for example if y = 3, then on the first iteration of the loop, x = 1 * 3 which equates to 3 and NOT 3! which equates to 6.
This is where my confusion really is I guess. Some books articles state that a loop invariant is a statement that must equate to true at the beginning or a loop (thus the precondition) and must also hold true at the end of the loop (thus post-condition) but does not necessarily need to hold true part-way through the loop.
What is the correct loop invariant for the function above?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（2）
一个可能的循环不变量是x⋅y！ = y0! 其中 y0 是传递给的 y 的初始值功能。无论循环已经完成了多少次迭代，此语句始终为真。
前置条件必须在循环开始之前成立，后置条件必须在循环结束后成立，并且无论循环进行了多少次迭代，不变式都必须成立（这就是为什么它被称为“不变式” - 它不'不改变它是真的）。
一般来说，同一个循环可能有不同的可能的不变量。例如，对于任何循环，1 = 1 作为不变量都是 true，但为了显示算法的正确性，您通常必须找到更强的不变量。
A possible loop invariant would be x⋅y! = y0! where y0 is the initial value of y that is passed to the function. This statement is always true, no matter how many iterations of the loop have already been done.
A precondition has to hold before the loop starts, a postconditions has to hold after the loop finishes, and an invariant has to hold no matter how many iterations of the loop have been done (that's why it's called "invariant" -- it doesn't change that it is true).
Generally, there might be different possible invariants for the same loop. For example 1 = 1 will be a true as a invariant for any loop, but to show correctness of an algorithm you usually will have to find a stronger invariant.
循环不变量可以从后置条件、一点直觉和一些类似代数的推理中导出。
您知道后置条件的一部分：
x == Y!，其中Y是作为参数给出的初始值。y是一个值会改变的变量。这就是后置条件的其余部分，顺便说一句：y == 1。每一次传递的真实情况是什么？推理倒退。
在最后一遍
x == Y*Y-1*...*2 和 y == 2。在那之前？
x == Y*Y-1*...*3 且 y == 3。在那之前？
当
y == Y时，最初的情况是什么？最后。给定后置条件和不变量，启动事物所需的最弱的一组语句是什么先决条件？代码表明，
x=1 且 y=Y。您知道，每次循环时，都必须发生一些变化，并且程序必须可证明将状态推进到后置条件。这是真的吗？是否存在循环状态的自然值函数，可证明其减小到零？ （这似乎是一个棘手的问题，因为 y 变量似乎微不足道。它在许多现实世界的循环中并不明显，因此您必须询问循环设计的问题。）
The loop invariant can be derived from the post condition, a little intuition and some algebra-like reasoning.
You know one part of the post condition:
x == Y!, whereYis the initial value given as an argument.yis a variable who's value changes. And that's the rest of the post condition, BTW:y == 1.What's true on each pass? Reason backwards.
On the last pass
x == Y*Y-1*...*2 and y == 2.Before that?
x == Y*Y-1*...*3 and y == 3.Before that?
What is true initially, when
y == Y?Finally. Given the post-condition and the invariant, what precondition is the weakest set of statements required to set things in motion? The code suggests,
x=1 and y=Y.You know that each time through the loop, something must change and the program must provably advance the state toward the post-condition. Is that true? Is there a natural-valued function of the loop state which provable decreases toward zero? (This seems like a trick question because the
yvariable seems to do that trivially. It's not obvious in many real-world loops, so you have to ask the question of your loop design.)