Dafny中序列类型的预期底层表示方式是什么

Dafny的语言规范本身没有对序列的运行时表示做强制约束，这和它不可变值的定位匹配：验证阶段只需要关注序列的逻辑语义，底层实现不会对验证结果产生任何影响。

目前官方针对不同编译目标的默认序列实现是公开的，不同实现的性能特征差异明显：

• 编译到C#、Java、Go、JavaScript这类命令式通用目标语言时，seq<T>默认采用对应语言的动态数组实现，随机访问的时间复杂度为O(1)，但取尾部、非末端拼接操作的时间复杂度为O(n)，需要完整复制涉及的元素
• 编译到F#、OCaml这类函数式目标语言时，Dafny提供了可选的链表实现方案，这种实现下取尾部操作为O(1)时间且不需要额外内存分配，拼接操作仅需重新分配左参数对应的节点，直接引用右参数即可，和常规函数式语言的列表实现逻辑一致

如果你的使用场景对序列操作的性能有明确要求，可以直接在Dafny的编译配置中指定序列的实现策略，不需要调整上层的业务逻辑代码。

提醒：仅当你需要将Dafny代码编译为可执行程序实际运行时，上述实现差异才有实际意义；如果仅使用Dafny做形式化验证，完全不需要关注这些内容。

内容的提问来源于stack exchange，提问作者Alley Stoughton