изменение возвращаемой переменной в dafny

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


dafny
person george    schedule 11.11.2020    source источник
comment
можешь опубликовать свой код?   -  person James Wilcox    schedule 11.11.2020

Ответы (1)


arrow_upward
0
arrow_downward

Массивы в 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]);

or

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

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

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

modifies a

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

person Rustan Leino    schedule 16.11.2020