问题标签 [invariants]

我用谷歌搜索了这个主题，但除了Wikipedia之外，我没有找到任何其他有用的文档或文章。

任何人都可以用简单的话向我解释它的含义或向我推荐一些易于理解的文档吗？

我正在研究一些 Hoare 逻辑，我想知道我的方法是否正确。

我有以下程序P：

它应该满足 hoare 三元组 {n >= 0}P{s = n*(n+1)/2} （所以它只需要总和）。现在，最初我有 |s = i*(i-1)/2| 作为我的不变量，效果很好。但是，从循环结束到我想要的后置条件，我遇到了问题。因为为了暗示

要持有，我需要证明 i 是 n+1，而不仅仅是任何大于 n 的 i。所以我想到的是在不变量中添加一个 (i <= n + 1) ，这样它就变成了：

然后我可以证明这个程序，所以我认为它应该是正确的。

尽管如此，我发现不变量有点“不变”:)。不像我在课程或练习中看到的任何东西，所以我想知道这里是否有更优雅的解决方案？

我不是 100% 确定三次幂求和中的不变量是什么。

注意：n 始终为非负值。

伪代码：

我知道它很乱，可以用更简单的方式完成，但这是我应该做的（主要用于算法分析实践）。

我要提出三个循环不变量；LI1、LI2 和 LI3。
我在想，对于 LI1，不变量与 tot=(i^2(i+1)^2)/4 （从 0 到 i 的平方和的方程）
我不知道要做什么为 LI2 或 LI3 做。LI2 的循环使 i^3 和 LI3 使 i^2，但我不完全确定如何将它们定义为循环不变量。

如果我在每个 while 循环体中都有 3 个单独的总变量，不变量会更容易定义吗？

谢谢你提供的所有帮助。

这个函数的增长顺序也是：Θ（n ^ 3）？

我不是 100% 确定三次幂求和中的不变量是什么。

注意：n 始终为非负值。

伪代码：

我知道它很乱，可以用更简单的方式完成，但这是我应该做的（主要用于算法分析实践）。

我要提出三个循环不变量；LI1、LI2 和 LI3。
我在想，对于 LI1，不变量与 tot=(i^2(i+1)^2)/4 （从 0 到 i 的平方和的方程）
我不知道要做什么为 LI2 或 LI3 做。LI2 的循环使 i^3 和 LI3 使 i^2，但我不完全确定如何将它们定义为循环不变量。

如果我在每个 while 循环体中都有 3 个单独的总变量，这些变量在第一个循环中 i++ 之前添加到主总数中，那么不变量会更容易定义吗？

谢谢你提供的所有帮助。

这些是求出数组 b[hk] 最小值的算法的断言：

这是这个不变量的正确循环吗？

不变量：b[x] 是 b[h...t] 的最小值

我正在尝试交换数组 b 的值并将一个值存储在 k 中，以便后置条件 b [0...h] <= 9 和 b[k+1..] > 9 为真。

到目前为止我有这个：

当我编写算法时，我通常会在注释中写下不变量。

例如，一个函数可能返回一个有序列表，而另一个函数期望一个列表是有序的。
我知道定理证明存在，但我没有使用它们的经验。

我也相信智能编译器 [原文如此！] 可以利用它们来优化程序。
那么，是否可以写下不变量并让编译器检查它们？

我想定义一个类型，以便所有构造都通过可以保留不变量的模块成员，但允许解构以进行模式匹配。

我只是在学习 OCaml，但以下几乎适用于具有左边应该严格小于右边的不变量的 int 对

这样有效

和时尚后的解构作品

构建失败时

但我真正想做的是具有解构元组的语法便利。以下不起作用：

但是我不能使用元组模式对其进行解构：

我可以将类型更改为，type t = R of (int * int)但我需要这些尽可能轻量级的内存。有任何想法吗？

在阅读加速 c++ 时，我对为什么不变量变为假的解释感到困惑（参见下面的代码）：

作者（在这种情况下）将不变量定义为：

我们的不变式是到目前为止我们已经写了 r 行输出。当我们定义 r 时，我们给它一个初始值 0。此时，我们还没有写任何东西。将 r 设置为 0 显然使不变量为真，因此我们满足了第一个要求。

然后后来解释...

写一行输出会导致不变量变为假，因为 r 不再是我们写的行数

鉴于定义，我无法在两者之间建立联系。

当一行输出正在写入时，为什么不变量会变为假？

我正在学习数据结构和算法的基础课程，我们使用的书是 CLRS 的开创性著作。我在理解循环不变量时遇到了一些麻烦，如第 2.1 章所述：插入排序。

书上说：

在第 1-8 行的 for 循环的每次迭代开始时，子数组 A[1..j -1] 由最初在 A[1..j-1] 中的元素组成，但按排序顺序。

现在，这让我很困惑。为什么在第一次迭代开始时会保持这种状态？假设要排序的数组看起来像 { 5, 2, 4, 6, 1, 3 }。现在，当 for 循环的第一次迭代开始时，A[1.. j-1] 不是按排序顺序排列的，但当迭代结束时它是有序的。

我在这里想念什么？