数组

我们所考虑的一切对于简单的函数和少量的数学练习来说都很好，但是对于真正的程序来说却毫无帮助。到目前为止，我们一次只考虑了局部变量中的几个值。现在我们把注意力转向数据数组。数组是语言的内置部分，有自己的类型array<T>，其中T是另一种类型。现在我们只考虑整数数组，array<int>。数组可以为null，并有一个内置的长度字段a. length。元素访问使用标准的括号语法，并从0开始索引，所以a[3]前面是3个元素 a[0]，a[1]和a[2]，按这个顺序。所有的数组访问必须被证明在边界内，这是Dafny无运行时错误安全保证的一部分。因为边界检查是在验证时验证的，所以不需要进行运行时检查。要创建一个新数组，它必须使用new关键字进行分配，但目前我们只使用以先前分配的数组为参数的方法。(有关分配的更多信息，请参阅内存教程。) 对于一个数组，我们可能想要做的最基本的事情之一是在数组中搜索一个特定的键，并返回一个位置的索引，如果键存在，我们可以找到它。我们有两个搜索结果，每个结果都有不同的正确性条件。如果算法返回一个索引(即非负整数)，那么该键应该存在于该索引处。这可以表示为:

method Find(a: array<int>, key: int) returns (index: int)
   ensures 0 <= index ==> index < a.Length && a[index] == key
{
   // Can you write code that satisfies the postcondition?
   // Hint: you can do it with one statement.
}
method Find(a: array<int>, key: int) returns (index: int)
   ensures 0 <= index ==> index < a.Length && a[index] == key
{
   // Open in editor for a challenge...
}

这里的数组索引是安全的，因为隐含操作符是短路。短路意味着如果左部分为假，那么不管第二部分的真值是多少，暗示已经为真，因此不需要求值。使用隐含运算符的短路特性，以及布尔值and(&&)，这也是一种短路，是Dafny的常见实践。条件index < a. length是必要的，否则该方法可能返回一个大整数，而不是数组的下标。总之，短路行为意味着当时间控制到达数组访问时，index必须是一个有效的索引。 如果该键不在数组中，那么我们希望方法返回一个负数。在这个例子中，我们想说这个方法没有丢失一个键的出现;换句话说，这个键不在数组中。为了表达这个属性，我们求助于另一个常用的Dafny工具:量词。