1

我正在尝试使用 Dafny 来验证一些非常简单的代码。第一块是普通版本。而且我只是找不到将后置条件设置为的方法

“存在我forall j ~~~~~~”

我不知道如何在 Dafny 中一起使用 2 个量词，请帮助。谢谢。

//this is a c++ version of the code
for (int lastNot0 = 0, cur = 0; cur < nums.length; cur++) {
    if (nums[cur] != 0) {
        swap(nums[lastNot0 ++], nums[cur]);
    }
}

//Dafny code
method moveZero(a: array<int>)
  requires a != null && a.Length > 0;
  modifies a;
  ensures exists i :: forall j :: 0 <= j < i < a.Length && a[j] != 0;
//  ensures forall k :: 0 <= k < a.Length && k != i && k != j ==> a[k] == old(a[k]);
{
  var lastNot0 := 0;
  var cur := 0;
  while(cur < a.Length)
  invariant 0 <= lastNot0 <= cur < a.Length
  {
    if(a[cur] != 0){
      swap(a, lastNot0, cur);
      lastNot0 := lastNot0 + 1;
    }
    cur := cur + 1;

  }
}

method swap(a: array<int>, i: int, j: int)
  requires a != null && 0 <= i < j < a.Length;
  modifies a;
  ensures a[i] == old(a[j]);
  ensures a[j] == old(a[i]);
  ensures forall k :: 0 <= k < a.Length && k != i && k != j ==> a[k] == old(a[k]);
{
  var temp := a[i];
  a[i] := a[j];
  a[j] := temp;
}
4

2 回答 2

0

我想你想说的是

ensures exists i | 0 <= i <= a.length ::
            forall j | 0 <= j < i ::  a[j] != 0 ;

但是，这是微不足道的（考虑 i==0），所以也许这不是你的意思。

从您的代码中，您将所有非零值移到前面。所以你还需要 i 及以后的项目为 0，所以

ensures exists i | 0 <= i <= a.length ::
               (forall j | 0 <= j < i ::  a[j] != 0)
            && (forall j | i <= j < a.length ::  a[j] == 0);

或更简洁地说

ensures exists i | 0 <= i <= a.length ::
            forall j | 0 <= j < a.length ::  a[j] != 0 <==> j < i ;
于 2017-03-02T00:14:00.757 回答
0

你的语法是正确的。问题是我们没有涉及i量词的条件。它只是这么说，i > j但与数组的值无关a。因此，您需要a[i] == 0在量词中添加另一个条件。

ensures exists i :: forall j :: 0 <= j < i < a.Length && a[j] != 0 && a[i] == 0;

这不会向您发出有关未找到触发条件的警告。

于 2017-02-24T23:03:34.397 回答