Dafny，调用可能会违反上下文的修改条款

Question

在我的程序（rise4fun 上的完整版）中，我想对数组进行切片，对每个切片进行排序，然后将它们合并回一起。

我选择使用序列，因为它使切片和合并变得非常容易。然后，为了重用一些现有代码，我将每个切片转换为数组并调用我的插入排序实现。但是调用报告 call may violate context's modifies clause 错误。这是为什么？

这是我的代码的主要部分。

method MySort(input:array?<int>)
modifies input;
requires input != null;
requires input.Length > 0;
requires input.Length%2==0;
{
if(input.Length%2!=0){return;}
 var mid:int := input.Length/2; 
 var subOne := input[0..mid];
 var subTwo := input[mid..input.Length];
 var arrSubOne := toArrayConvert(subOne);
 var arrSubTwo := toArrayConvert(subTwo);
 insertionSort(arrSubOne); //call may violate context's modifies clause
 insertionSort(arrSubTwo); //call may violate context's modifies clause
} 

method toArrayConvert(s:seq<int>) returns(a:array<int>)
requires |s|>0;
ensures |s| == a.Length;
ensures multiset(s[..]) == multiset(old(s[..]))
ensures forall i::0<=i<a.Length ==> s[i] == a[i];
{ /* ... */ }

method insertionSort(input:array?<int>)
modifies input
requires input != null
requires input.Length > 0
ensures perm(input,old(input))
ensures sortedBetween(input, 0, input.Length) // 0 to input.Length = whole input
{ /* ... */ }

Answer 1

这个问题很难回答，因为你没有提供insertionSort的合同。我的猜测是 insertionSort 修改的比它的调用者多，即 insertionSort 在其 modifies 子句中列出了一些 MySort 未在其 modifies 子句中列出的数据.

如果这被允许，那么 MySort 的调用者将 "miss" 潜在的修改，因为 MySort 的合同只是一个欠近似，这是不合理的。

Answer 2

您缺少 toArrayConvert

的后置条件

ensures fresh(res)

然后你的整个程序都会验证。

这个后置条件保证该方法返回的数组是"fresh"，这意味着它是新分配的。这让达夫尼得出结论，你没有修改任何你不应该修改的东西：你可以修改数组，因为你分配了它！

请提出一个关于序列交换的单独问题，或者如果您觉得答案不够充分，请更新关于该主题的旧问题。

Dafny，调用可能会违反上下文的修改条款

Dafny, call may violate context's modifies clause

verification

dafny