1

因此，我尝试在 Dafny 中实现一个简化的荷兰国旗问题的程序，其中所有索引 0 <= n < k 都是红色的，所有索引 k <= n < arr.Length 都是蓝色的，除了它一直说 k 可能会消失即使根据我的编码方式，它最多应该是 arr.Length 。我在这里做错了什么？

method dutch(arr: array?<char>) returns (k: int)
requires arr != null && forall x :: 0 <= x < arr.Length ==> arr[x] == 'r' || arr[x] == 'b'
ensures k <= arr.Length     //postcondition might not hold
ensures forall n :: 0 <= n < k ==> arr[n] == 'r'     //out of range
ensures forall n :: k <= n < arr.Length ==> arr[n] == 'b'     //out of range
modifies arr
{
  var x := 0;
  k := 0;
  while(x < arr.Length)
  invariant k <= x
  invariant forall n :: 0 <= n < k ==> arr[n] == 'r'     //out of range
  invariant forall n :: k <= n < x ==> arr[n] == 'b'     //invariant might not be maintained by loop
  {
    if(arr[x] == 'r')
    {
      arr[x] := arr[k];
      arr[k] := 'r';
      k := k + 1;
    }
    x := x + 1;
  }
}
4

1 回答 1

1

在循环之后，所知道的只是循环保护的不变量和否定。所以，arr.Length <= x成立，也是如此k <= x。因此，根据您的循环规范，x可能是arr.Length + 10并且k可能是arr.Length + 2.

要验证程序，您需要将k“最多应arr.Length基于我的编码方式”的信念转变为循环规范。所以，添加

invariant k <= arr.Length
于 2021-03-03T18:21:49.867 回答