问题标签 [loop-invariant]

我有一个非常简单的函数，它应该以给定的时间单位计算两个日期之间的时间量，例如：getPartialPeriod(January 1, February 15, months)将导致1.5.

我真的很纠结如何证明它——我从循环开始，因为我认为这是最困难的部分。我定义了许多 Hoare 三元组和循环不变量，却发现它们都没有用。我会很感激我能得到的所有帮助。

函数伪代码：

PS请忽略这似乎是一个愚蠢的实现 - 这并不重要。

CLRS 说

我们必须展示关于循环不变量的三件事：

• 初始化：在循环的第一次迭代之前为真。
• 维护：如果在循环的迭代之前为真，则在下一次迭代之前保持为真。
• 终止：当循环终止时，不变量为我们提供了一个有用的属性，有助于证明算法是正确的。

我的问题是我可以编辑这些步骤并改为：

• 初始化：在循环的第一次迭代之后为真。
• 维护：如果循环一次迭代后为真，则在下一次迭代后仍为真。
• 终止：当循环终止时，不变量为我们提供了一个有用的属性，有助于证明算法是正确的。

说明：基本上我们使用数学归纳原理来证明正确性。使用“初始化”，我们证明该属性在第一次迭代后成立。使用“维护”，我们可以证明该属性适用于所有迭代，因为“初始化”和“维护”一起创建了一个链。因此，该属性在最后一次迭代后也成立。

例子：

对于这个算法，教科书中已经有一个使用标准程序给出的证明（因为太长了，我没有在这里包含它）。

我的建议：

• 循环不变量：就在第2-3 行的 for 循环的第 i^次迭代之后，对于每个可能的 (i)-排列，子数组 A[1 .. i] 包含这个 (i)-排列，概率为 (n - i )!/n!。
• 初始化：在第 1^次迭代之后，A[1] 包含这个排列，概率为 (n-1)!/n!=1/n，这是真的。
• 维护：让它在第 (i-1)^次迭代之后为真。在第 (i)^次迭代之后，A[1...i] 包含这个排列的概率为 [(n-i+1)!/n!]*[1/(n-i+1)]=(ni)! /n！这就是我们想要的。
• 终止：在终止时，i = n，我们有子数组 A[1 .. n] 是一个给定的 n 排列，概率为 (n - n)!/n! = 1/n!。因此，RANDOMIZE-IN-PLACE 产生一个统一的随机排列。

我的解释合乎逻辑吗？

任何帮助将不胜感激。谢谢。

我读过循环不变量，但我有点困惑。
假设我有这段代码，不变量是什么？像 A+B =X 这样的东西？

给定一个循环不变量，维基百科列出了一个为循环生成最弱前提条件的好方法（来自http://en.wikipedia.org/wiki/Predicate_transformer_semantics）：

M[x <- N] 用 N 替换 M 中所有出现的 x。

现在，我的问题是变量 y。\forall y, 在表达式中绑定 y，因此“y 是新变量的元组”不会为我解析。\forall 中的 y 是否与 "[x <- y]" 中的 y 相同？我根本无法解析上述内容。

编辑：改写以避免参考请求。

我的问题是：循环不变量和计算最弱前提（如果有的话）之间的直接联系是什么。似乎在实践中所做的很多事情都将循环的最弱前提条件放松为适合验证的前提条件。来自维基百科的上述内容表明，给定一个循环不变量，确实可以计算出鼻子上最弱的先决条件，但我无法理解这个条件。

在我的计算理论课程中，我很难掌握证明迭代程序/函数正确性的概念。更具体地说，我不知道如何提出循环不变量。我知道一个函数可以有多个循环不变量，但对我来说如何找到一个可以帮助我们证明后置条件的完全是个谜。我目前正在做一些功课，不知道如何找到以下函数的循环不变量。

到目前为止，我了解该函数的工作原理，但正如我之前所说，当我试图找到一个合适的循环不变量来帮助我证明这个函数返回 a^b 时，我非常迷茫。

对于分配，我必须创建一个使用二进制搜索来查找整数的平方根的方法，如果它不是平方数，它应该返回一个整数 s 使得 s*s <= 数字（所以对于 15 它将返回 3)。到目前为止我的代码是

这会为平方数返回正确的数字，但会陷入其他整数的无限循环。我知道问题出在 while 条件下，但由于平方数之间的差距随着数字变大而变得越来越大（所以我不能只说差距必须低于一个阈值）。如果有帮助的话，这个练习是关于不变量的（因此为什么要以这种方式设置）。谢谢你。

我需要 hep 弄清楚这段代码的不变量是什么。我认为可能有多个不变量，但我并不真正理解我发现的主题和在线资源仍然没有真正的帮助。我为二进制搜索制作的代码是：

此代码使用二进制搜索来查找整数的平方根，但如果它不是平方数，它应该返回小于整数的最接近平方数的平方根。

该代码有效，但我只是真正得到了作为不变量放置的内容以及它如何显示要返回的正确值是什么。任何线索/解释都会很棒，谢谢。

所以我正在编写这个程序，将用户输入存储在链表上并将其反转，但我有点迷茫。是否可以为不返回任何值的循环类型提供循环不变量？例如，位于 main 内部的循环。

这是我用来在 main 中获取用户输入并将其存储在链表中的循环示例，当然代码上还有更多内容，但我只展示了相关的内容。

是否有可能为此提出一个循环不变量？另外，程序正确性是什么意思，在我的情况下如何证明它？

谢谢！

我有一个 while 循环（如下所示），它不断地从文件中读取，直到达到 EOF。我应该为任何非平凡的循环编写一个循环不变量。这是一个微不足道的循环吗？如果不是，那么这个 while 循环的循环不变量是什么？我以前从未写过不变量。

我有以下代码来反转整数中的数字：

我的教授要求我们编写这段代码，还说要编写循环不变量和循环条件。我理解这里的循环条件，我只是不确定我应该看什么不变量。我意识到在 while 循环的开始和结束时某些条件是正确的，对于每次迭代，我只是看不出它会是什么。提示将不胜感激。