继续获取“索引超出范围”

【问题标题】：Keep Getting "Index Out of Range"继续获取“索引超出范围”
【发布时间】：2021-06-01 05:16:25
【问题描述】：

所以我尝试在 Dafny 中实现一个简化的荷兰国旗问题的程序，其中所有索引 0

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;
  }
}

【问题讨论】：

标签： arrays indexoutofboundsexception dafny dutch-national-flag-problem

【解决方案1】：

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

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

invariant k <= arr.Length

【讨论】：