很明显
，输入是一个数组，但是为什么当它进行flag[1..]时，它说flag是一个序列？这是链接：http://rise4fun.com/Dafny/fUgu
对于数组A和整数lo和hi，表达式A[lo..hi]从索引lo开始返回A hi-lo元素的序列(不是数组(。 对于您的程序，我建议要么让所有函数都对序列进行操作，要么(可能对您的程序更好(向所有函数添加lo和hi参数，以描绘您感兴趣的数组部分。