如何在Dafny中获取数组的长度？

Dafny是大小写敏感的语言，原生数组的长度属性是**arr.Length**（注意首字母大写），你之前尝试的小写arr.length或者arr.size()都是错误写法。

下面是演示正确用法的示例代码：

method TestArrayLength() {
    // 创建一个长度为7的整数数组
    var myArray := new int[7];
    // 打印数组长度
    print "数组长度为: ", myArray.Length, "\n";
}

如果arr.Length仍无法生效，可能是以下原因：

• 你操作的不是Dafny原生数组，而是序列（seq类型）。序列的长度需要用|seqVar|获取，比如var s := [1,2,3]; print |s|;会输出3。
• 变量arr的类型不是数组，或者未完成正确初始化。

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