Dafny调用insertionSort触发modifies clause违规错误原因排查

这个错误的核心是Dafny的方法契约检查机制在起作用——你必须严格遵守自己声明的方法修改权限，否则它会阻止你调用那些修改未授权对象的方法。咱们一步步拆解问题：

首先看你的MySort方法声明：

method MySort(input:array?<int>) modifies input;

这里你明确告诉Dafny：这个方法只会修改传入的input数组，不会触碰其他任何对象。

但接下来你做了两件关键的事：

1. 通过toArrayConvert创建了两个全新的数组arrSubOne和arrSubTwo
2. 调用insertionSort去修改这两个新数组

而insertionSort的声明是：

method insertionSort(input:array?<int>) modifies input

它明确表示会修改自己的参数数组。

问题就出在这里：arrSubOne和arrSubTwo是MySort内部创建的新数组，不在MySort声明的modifies列表里。Dafny会严格检查：当你在一个方法里调用另一个方法时，被调用方法要修改的所有对象，必须都在当前方法的modifies允许范围内。否则就会抛出"call may violate context's modifies clause"错误——因为你承诺MySort只改input，但实际要改其他数组，违反了自己的契约。

解决办法 #

有两种常见的修复方式，你可以根据需求选择：

1. 扩大MySort的修改权限范围

如果你确实需要在MySort里创建并修改新数组，可以把modifies子句改成允许修改方法内分配的所有对象，用*来表示：

method MySort(input:array?<int>) modifies input, *;

这里的*代表“当前方法中分配的任何对象”，刚好覆盖你用toArrayConvert创建的两个局部数组。

如果你想更精确（避免不必要的权限扩大），也可以明确列出要修改的局部数组：

method MySort(input:array?<int>) modifies input, arrSubOne, arrSubTwo;

因为arrSubOne和arrSubTwo是方法内的局部变量，Dafny同样会认可这种声明。

2. 避免创建新数组，直接操作原数组切片

如果你不需要新数组，而是想直接在原input的前半段和后半段排序，可以调整insertionSort的参数，让它接受数组和起止索引：

method insertionSort(input:array?<int>, start:int, end:int) 
  modifies input
  requires input != null
  requires 0 <= start < end <= input.Length
  ensures perm(input, old(input))
  ensures sortedBetween(input, start, end)
{
  // 实现只排序start到end-1区间的元素
}

然后在MySort里直接调用：

insertionSort(input, 0, mid);
insertionSort(input, mid, input.Length);

这种方式不需要创建新数组，完全符合原MySort的modifies input声明，自然不会触发错误。

总结 #

本质上，这个错误是Dafny在帮你维护代码的可验证性——它确保你严格遵守自己声明的修改权限，防止方法偷偷修改未声明的对象。只要让MySort的modifies子句覆盖所有它实际要修改的对象，问题就解决了。

内容的提问来源于stack exchange，提问作者Amir-Mousavi