1

我试图在 dafny 中证明这个程序，但我仍然得到最后一个不变量的错误，我不明白为什么它不起作用。

该程序包含一个将 int 插入排序数组的方法。int 将插入正确的位置，即：将 5 插入 1,2,3,4,5,6,7 将返回：1,2,3,4,5,5,6,7

function sorted (a: array<int>): bool
  requires a != null ;
  reads a;
  {
    forall i :: 0 <= i < (a.Length - 1) ==> a[i] <= a[ i+1]
  }

method InsertSorted(a: array<int>, key: int ) returns (b: array<int>)
  requires a != null && sorted(a);
  ensures b != null ;
  ensures sorted(b);
   {
     var i:= 0;
     b:= new int[a.Length + 1];

     if(a.Length > 0){
      while (i < a.Length)
      invariant 0<= i;
      invariant i <= a.Length;
      invariant b.Length == a.Length + 1;
      invariant sorted(a);
      invariant forall j :: 0 <= j < i ==> b[j] <= b[j+1];
      {
        if(a[i]<=key)
        {
          b[i]:= a[i];
          b [i+1] := key;
          assert b[i] <= b[i+1];         
        }
        else if (key > a[i])
        {
          if(i==0)
          {
            b[i] := key;
          }
          b [i+1] := a[i];
          assert key > a[i];
          assert b[i]<= b[i+1];
        }
        else{
          b[i]:= a[i];
          b [i+1] := a[i];
          assert sorted(a);
          assert b[i] <= b[i+1];
        }
        assert b[i]<= b[i+1];
        i := i+1;
      }
     }
     else{
       b[0] := key;
     }
   }

谢谢

4

1 回答 1

1

我认为也许你的算法不正确。无论如何，我发现条件很难理解，如果第一个分支没有被采用，那么我们知道!(a[i] <= key)或者更简单地说a[i] > key，这意味着第二个分支key > a[i]是不可访问的。

!(a[i]<=key) && a[i] < key ==> false

无论如何，我怀疑循环不变量不足以证明甚至是正确的版本，因为您没有b足够详细地跟踪状态。

下面是与您的算法相似的算法的证明，显示了更强的循环不变量。key我使用幽灵变量（仅用于验证且不会出现在编译器输出中的变量）跟踪数组中插入的位置。

http://rise4fun.com/Dafny/RqGi

predicate sorted (a: seq<int>)
{
 forall i,j :: 0 <= i < j < |a| ==> a[i] <= a[j]
}

predicate lessThan(a:seq<int>, key:int) {
 forall i :: 0 <= i < |a| ==> a[i] < key
}

predicate greaterEqualThan(a:seq<int>, key:int) {
 forall i :: 0 <= i < |a| ==> a[i] >= key
}

method InsertSorted(a: array<int>, key: int ) returns (b: array<int>)
  requires a != null && sorted(a[..])
  ensures b != null && sorted(b[..]);
{
 b:= new int[a.Length + 1];

 ghost var k := 0;
 b[0] := key;

 ghost var a' := a[..];

 var i:= 0;
 while (i < a.Length)
  modifies b;
  invariant 0 <= k <= i <= a.Length
  invariant b.Length == a.Length + 1
  invariant a[..] == a'
  invariant lessThan(a[..i], key) ==> i == k;
  invariant lessThan(a[..k], key)
  invariant b[..k] == a[..k]
  invariant b[k] == key
  invariant k < i ==> b[k+1..i+1] == a[k..i]
  invariant k < i ==> greaterEqualThan(b[k+1..i+1], key)
  invariant 0 <= k < b.Length && b[k] == key
  {
    if(a[i]<key)
    {
      b[i]:= a[i];
      b[i+1] := key;
      k := i+1;
    }
    else if (a[i] >= key)
    {
      b[i+1] := a[i];
    }
    i := i+1;
  }
  assert b[..] == a[..k] + [key] + a[k..];

}

于 2016-01-07T22:59:47.933 回答