Лучший способ обновить неизменяемую строку в dafny

Я пытаюсь проверить программу, которая применяет шифр Цезаря к строке. Исходная строка должна быть возвращена

method caesar(s:string, index:int)
//apply caesar

Каков наилучший способ обновить значение строки, например:

s[i] := 'x'

string immutability dafny
person rohaldb    schedule 11.05.2016    source источник

Ответы (1)


arrow_upward
2
arrow_downward

В Dafny нет возможности обновить строку. Строки представлены как seq<char> , а последовательности неизменяемы в Dafny. Неизменяемость означает, что последовательность является значением и не может быть изменена.

Если вам нужно выполнить манипуляцию на месте вместо этого вы можете использовать array<char>.

Если вы можете вернуть новую последовательность ты можешь сделать

var s' := s[i := e];
return s';
person lexicalscope    schedule 11.05.2016