Dafny：为什么我输入一个数组 Dafny 说它是一个序列

【问题标题】：Dafny: Why I input an array Dafny says it is a sequenceDafny：为什么我输入一个数组 Dafny 说它是一个序列
【发布时间】：2017-10-21 03:15:21
【问题描述】：

很清楚输入是一个数组，但是为什么在执行flag[1..]时，它说flag是一个序列？链接在这里： http://rise4fun.com/Dafny/fUgu

【问题讨论】：

【解决方案1】：

对于数组A 和整数lo 和hi，表达式A[lo..hi] 从A 返回hi-lo 元素的序列（不是数组），从索引lo 开始。对于您的程序，我建议让您的所有函数在序列上运行，或者（可能对您的程序更好）将lo 和hi 参数添加到所有函数中，以描绘您感兴趣的数组部分。

【讨论】：

@Lilac Liu，嗨，我也在 Dafny 的 seq 和 array 方面苦苦挣扎。您是否找到了将 seq 转换为数组的方法？
方法 SeqToArray(s: seq) 返回 (a: array) 确保新鲜(a) && a[..] == s { a := new T [|s|](i 需要 0 s[i]); }