Блог

итак, у меня есть метод в dafny, который принимает массив a и возвращает отсортированную версию, b. В моем коде b := a, а затем для b выполняется сортировка по вставке на месте. Однако всякий раз, когда я изменяю b, я получаю сообщение об ошибке, что «присваивание может обновить элемент массива, которого нет в предложении modifies заключающего контекста». Я предполагаю, что это потому, что я не сказал dafny, что я буду на месте изменять b. Как мне это исправить?

Массивы в Dafny являются ссылками на элементы массива. (Это также имеет место в C, Java, C # и различных других языках.) Присваивание b := a; копирует ссылку, но не копирует элементы. У вас есть два варианта.

Один из вариантов — создать новый массив, который в конечном итоге будет содержать отсортированные элементы. Для этого выделите новый массив:

 b := new int[a.Length];
  

Если вы также хотите скопировать элементы a в новый массив b , выполните:

 b := new int[a.Length](i requires 0 <= i < a.Length reads a => a[i]);
  

или

 b := new int[a.Length];
forall i | 0 <= i < a.Length {
  b[i] := a[i];
}
  

При этом выборе вызывающий объект по-прежнему будет иметь ссылку на исходный массив, который будет сохранен. Через out-параметр метода вызывающий объект также получит ссылку на новый (отсортированный) массив.

Другой вариант — изменить исходный массив. Поскольку это влияет на вызывающий объект, вам необходимо написать спецификацию, которая сообщает вызывающему объекту об этом. Это делается путем добавления

 modifies a
  

в соответствии со спецификацией вашего метода. При этом выборе нет причин объявлять out-параметр b , поскольку существует только один массив и a ссылается на него.