Dafny, call may violate context's modifies clause

Question

In my program (full version on rise4fun), I want to slice an array, sort each slice, and then merge them back together.

I chose to use sequences because it makes slicing and merging very easy. Then, in order to reuse some existing code, I convert each slice to an array and call my implementation of insertion sort. But the call reports a call may violate context's modifies clause error. Why is that?

Here is the main portion of my code.

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

You are missing a postcondition on toArrayConvert

ensures fresh(res)

Then your whole program verifies.

This postcondition guarantees that the array returned by that method is "fresh", meaning it is newly allocated. That allows Dafny to conclude that you are not modifying anything you're not supposed to: you're allowed to modify the array because you allocated it!

Please ask a separate question about the sequence swapping, or update your old question about that topic if you felt the answer was not sufficient.