Дафни, замени индекс на значение в последовательностях

в руководстве по Dafny по адресу rise4fun s[i := v] определяется для замены индекса i на v в последовательности s . но использование этого всегда терпит неудачу с expected method call, found expression.

например, в приведенном ниже коде для замены двух индексов

var a:int :=input[j];
var b:int :=input[j-1];
input[j := b]; //expected method call, found expression
input[j-1 := a]; //expected method call, found expression

как правильно использовать s[i := v] в случае замены двух индексов.


verification z3 dafny
person Amir-Mousavi    schedule 19.05.2018    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Вы могли бы написать

var a:int :=input[j];
var b:int :=input[j-1];
input := input[j:=b] ;
input := input[j-i : a];

Более кратко, но, возможно, труднее читать

input := input[ j := input[j-1] ][ j-1 := input[j] ] ;
person Theodore Norvell    schedule 21.05.2018
comment
Спасибо, но выдает ошибку: LHS присваивания должен обозначать изменяемую переменную. На самом деле я не хочу создавать еще одну локальную переменную, потому что это создает много проблем для остальной части программы. есть ли способ сделать на месте подкачки? - person Amir-Mousavi; 22.05.2018
comment
Это потому, что index не является изменяемой переменной. Правильное решение - сделать еще одну переменную. (См. stackoverflow.com/questions/50440756/.) Для замены на месте используйте массив, а не последовательность. - person Theodore Norvell; 23.05.2018