问题标签 [loop-invariant]

我目前在我的家庭作业中陷入循环不变证明。我需要证明其正确性的算法是：

我试着看几个循环不变量的例子，我对它应该如何工作有了一些了解。然而，在上面的这个算法中，我有两个退出条件，我对如何在循环不变证明中处理这个问题有点迷茫。特别是我正在努力解决的终止部分，围绕 IF 和 ELSE 语句。

到目前为止，我所构建的只是查看算法的终止，在这种情况下，如果x = 0它返回y包含n(while 循环中的迭代次数) 的值的值，其中 if xis not 0，x < b然后它返回-1。我只是有一种感觉，我需要以某种方式证明这一点。

我希望有人可以为我提供一些帮助，因为我在这里找到的类似案例还不够。

非常感谢您抽出宝贵的时间。

假设这个算法给出了一个子数组的最大和。并设 a[] 为长度为 n 的数组。

我怎样才能找到一个循环不变量，它在执行之前，当然在循环迭代之前和之后都成立，当 n-1 时，不变量应该暗示正确的解决方案。

我需要用给定的规范构造和证明一个循环不变量：

其中|A| 是集合 A 的元素数。这意味着q等于数组a中等于x的元素数。

代码P指定为：

我知道循环不变量必须是真的：

• 在循环开始之前
• 在循环的每次迭代之前
• 循环结束后

但我不知道如何找到正确的循环不变量，这将允许我在之后显示 P 的部分正确性。我已经尝试查看循环的每一次迭代以及随机n、x和a[0...n-1] 的变量，以查看在循环工作时哪些组合的值是恒定的，但这没有帮助。

I've been trying to get each character from every String by column but I only got the first characters of every string, I want to get every character by column from every string.

For example:

I have three strings from ArrayList of Strings:

1. chi
2. llo
3. ut

What I want to happen must be like this, after getting each character by column from strings:

1. clu
2. hlt
3. io

So long, my current source code only gets the first characters of first two string which is 'cl', Here's my current source code:

我试图了解循环不变量如何与中断相互作用。CLRS 3e (pg19) 将循环不变量描述为要求

如果在循环的迭代之前为真，则在下一次迭代之前它仍然为真。

所以给定以下简单的循环

可以说i < 4是循环的不变属性吗？论点是，由于循环在break语句处终止，因此在违反该属性后没有迭代。

我正在尝试为以下while循环提出一个循环不变量，但是遇到了一些麻烦。

确定循环不变量后，我想整理一个证明表并显示所有中间断言

我在为快速排序算法的某些实现定义和证明循环不变量时遇到了麻烦。这既不是 Lomuto 也不是 Hoare 的分区版本。

如果您知道以这种方式实现的某些已知版本的 Quicksort，请告诉我。

算法在 Python 中的实现：

我设法定义了以下循环不变量（它可能不正确）：

在循环的每次迭代开始时，对于arraywhile中的每个索引：kA

• 如果k = p，那么A[k] = y

• 如果p < k <= i，那么A[k] < y

• 如果j <= k <= r，那么A[k] > y

请帮我为方法中的while循环定义一个循环不变量partition()（如果上面不正确的话），并证明它。

我正在关注 codecontracts 教程（https://docs.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts#usage-guidelines），但我似乎无法让最简单的事情正常工作. 给定方法定义

当我调用o.Add(0,0)该方法时，前置条件检查不会失败。当我处于调试模式时，Contract.Requires()会跳过这些语句。我在哪里做错了？

第二个问题可以Contract.Invariant()用来检查循环不变量吗？根据对象不变量的定义，Object invariants are conditions that should be true for each instance of a class whenever that object is visible to a client.这似乎与循环不变量有点不同，因为在每次循环迭代中，循环不变量可能不一定对客户端可见，因此它可能违反属性但未被检查。这种理解正确吗？

我试图在 Dafny 中证明一个简单的程序，它可以找到整数数组的最大元素。Dafny在几秒钟内成功地证明了下面的程序。当我从最后两个规范中删除注释ensures时，Dafny 会发出错误消息说

这可能是由index保证为<= a.Length. 但是，max_index < a.Length是正确的，我很难证明这一点。我尝试在语句中编写嵌套不变量if，但 Dafny 拒绝了该语法。任何可能的解决方案？这是我的代码：

我试图证明gcdDafny 中的简单算法，所以我写了以下内容，但似乎我不能divides在循环不变量中使用该方法：

无论如何divides在不变量中使用方法/函数/宏？