string - dafny で不変の文字列を更新する最良の方法

Question

文字列にシーザー暗号を適用するプログラムを検証しようとしています。元の文字列を返す必要があります

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

次のように、文字列の値を更新する最良の方法は何ですか?

s[i] := 'x'

Answer 1

Dafny で文字列を更新する方法はありません。文字列は として表されseq<char>、シーケンスは Dafny では不変です。不変とは、シーケンスが値であり、変更できないことを意味します。

その場で操作する必要がある場合は、代わりに を使用できますarray<char>。

新しいシーケンスを返すことができる場合は、次のことができます

var s' := s[i := e];
return s';