В моей программе (полная версия на 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
{ /* ... */ }