string - 在 dafny 中更新不可变字符串的最佳方法

Question

我正在尝试验证一个将凯撒密码应用于字符串的程序。必须返回原始字符串

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

更新字符串值的最佳方法是什么，类似于：

s[i] := 'x'

Answer 1

在 Dafny 中无法更新字符串。字符串表示为seq<char>，而序列在 Dafny 中是不可变的。不可变意味着序列是一个值并且不能更改。

如果您需要进行就地操作，您可以使用 anarray<char>代替。

如果您可以返回一个新序列，您可以这样做

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