标签: loop-invariant

我正在阅读CLRS的"算法简介".在第2章中,作者提到了"循环不变量".什么是循环不变量？

如算法简介(http://mitpress.mit.edu/algorithms)所示,练习陈述如下:

输入:数组A [1 ... n]

输出:i,其中A [i] = v或未找到时为NIL

为LINEAR-SEARCH写一个伪代码,它扫描序列,寻找v.使用循环不变量,证明你的算法是正确的.(确保你的循环不变量满足三个必要的属性 - 初始化,维护,终止.)

我没有创建算法的问题,但我没有得到的是我如何决定我的循环不变量.我认为我理解了循环不变量的概念,即在循环开始之前,在每次迭代的结束/开始时始终为真的条件,并且当循环结束时仍然为真.这通常是目标,例如,在插入排序时,迭代j,从j = 2开始,[1,j-1]元素始终排序.这对我来说很有意义.但对于线性搜索？我想不出任何东西,想到循环不变只是听起来太简单了.我明白了什么问题吗？我只能想到一些明显的东西(它是NIL或介于0和n之间).非常感谢提前!

考虑解决100名囚犯的标准策略和灯泡问题.这是我在Dafny模拟它的尝试:

method strategy<T>(P: set<T>, Special: T) returns (count: int)
  requires |P| > 1 && Special in P
  ensures count == (|P| - 1)
  decreases *
{
  count := 0;
  var I := {};
  var S := {};
  var switch := false;

  while (count < (|P|-1)) 
    invariant count <= (|P|-1) 
    invariant count > 0 ==> Special in I
    invariant Special !in S && S < P && S <= I && I <= P 
    decreases *
  { …

当使用形式方面来创建一些代码时,是否有一种确定循环不变量的通用方法,或者它是否会根据问题完全不同？

我正在研究Hoare Logic,我在理解寻找循环不变量的方法时遇到了问题.

有人可以解释用于计算循环不变量的方法吗？

循环不变量应该包含什么才能成为"有用的"？

我只是处理简单的例子,找到不变量并在例子中证明部分和完全的纠正:

{ i ? 0 } while i > 0 do i := i?1 { i = 0 }

我读过多篇文章,包括关于二元搜索的Jon Bentleys章节.这就是我对CORRECT二进制搜索逻辑的理解,它在我做的简单测试中起作用:

binarysearch (arr, low, high, k)
    1. while (low < high)
        2. mid  = low + (high - low)/2
        3. if (arr[mid] == k)
               return mid
        4. if (arr[mid] < k )
               high = mid -1
        5. else 
               low = mid + 1

现在要找到第一次出现的已排序的重复项,如果条件继续而不是返回mid,那么你就有机会第3行

binarysearch_get_first_occur_with_duplicates (arr, low, high, k)
    1. while (low < high)
        2. mid  = low + (high - low)/2
        3. if (arr[mid] == k)
               high = mid - 1
               low_so_far = arr[mid]
        4. if (arr[mid] < …

什么是循环不变量,如何使用它们来证明堆排序算法的正确性？

我很难正确识别以下函数的循环不变量:

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和NOT 3!相当于6.

这就是我猜想我的困惑.一些书籍文章声明循环不变量是一个必须在开头或循环(因此是前置条件)等于true的语句,并且必须在循环结束时保持为真(因此在条件后)但不一定需要在循环中保持正常.

上述函数的正确循环不变量是多少？

我无法证明2个循环不变量:

    loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m2)[i] == \at(((char*)m1)[i], Pre);
    loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m1)[i] == \at(((char*)m2)[i], Pre);

我猜测\对于阵列不起作用,正如我所料.

ACSL by Example(第68页,swap_ranges)中有一个类似的函数,它使用了这个函数,但是如上所述,它们无法用WP插件证明这个特定的函数.我在我的机器上试过它,实际上它无法证明相同的不变量.

完整代码

/*
 * memswap()
 *
 * Swaps the contents of two nonoverlapping memory areas.
 * This really could be done faster...
 */

#include "string.h"

/*@
    requires n >= 1;
    requires \valid(((char*)m1)+(0..n-1));
    requires \valid(((char*)m2)+(0..n-1));
    requires \separated(((char*)m1)+(0..n-1), ((char*)m2)+(0..n-1));
    assigns ((char*)m1)[0..n-1]; …

我正在尝试在 Spark 中编写代码，使用 Horner 方法计算多项式的值。变量Result由Horner计算，变量Z以经典方式计算。我做了很多不同的测试，我的循环不变式总是正确的。但是，我收到消息：

loop invariant might not be preserved by an arbitrary iteration

是否存在循环不变量不起作用的情况，或者您是否需要向不变量添加更多条件？

这是我的主函数，它调用我的 Horner 函数：

  with Ada.Integer_Text_IO;
  use Ada.Integer_Text_IO;

  with Poly;
  use Poly;

  procedure Main is
     X : Integer;
     A : Vector (0 .. 2);
  begin
     X := 2;
     A := (5, 10, 15);

     Put(Horner(X, A));
  end Main;

和霍纳函数：

package body Poly with SPARK_Mode is
function Horner (X : Integer; A : Vector) 
  return Integer 
  is

  Result : Integer := 0;
  Z …